Let  be a 
basis
of
 be a 
basis
of  . On one hand, we can extend this basis, according to
fact,
to a basis
. On one hand, we can extend this basis, according to
fact,
to a basis  of
 of  , on the other hand, we can extend it to a basis
, on the other hand, we can extend it to a basis  of
 of  . Then
. Then
-    
is a
generating system
of  . We claim that it is even a basis. To see this, let
. We claim that it is even a basis. To see this, let
-   
This implies that the element
-   
belongs to  . From this, we get directly
. From this, we get directly
 for
for
 ,
and
,
and
 for
for
 .
From the equation before, we can then infer that also
.
From the equation before, we can then infer that also
 holds for all
holds for all  . Hence, we have  
linear independence.
This gives altogether
. Hence, we have  
linear independence.
This gives altogether
