let V be RealLinearSpace; :: thesis: for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

let W be Subspace of V; :: thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

let L be Linear_Combination of V; :: thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L ) )

assume A1: Carrier L c= the carrier of W ; :: thesis: ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

then reconsider C = Carrier L as finite Subset of W ;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider K = L | the carrier of W as Function of the carrier of W,REAL by FUNCT_2:32;

A2: K is Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8;

A3: dom K = the carrier of W by FUNCT_2:def 1;

take K ; :: thesis: ( Carrier K = Carrier L & Sum K = Sum L )

thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th10; :: thesis: verum

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

let W be Subspace of V; :: thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds

ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

let L be Linear_Combination of V; :: thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L ) )

assume A1: Carrier L c= the carrier of W ; :: thesis: ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum K = Sum L )

then reconsider C = Carrier L as finite Subset of W ;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider K = L | the carrier of W as Function of the carrier of W,REAL by FUNCT_2:32;

A2: K is Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8;

A3: dom K = the carrier of W by FUNCT_2:def 1;

now :: thesis: for w being VECTOR of W st not w in C holds

K . w = 0

then reconsider K = K as Linear_Combination of W by A2, RLVECT_2:def 3;K . w = 0

let w be VECTOR of W; :: thesis: ( not w in C implies K . w = 0 )

A4: w is VECTOR of V by RLSUB_1:10;

assume not w in C ; :: thesis: K . w = 0

then L . w = 0 by A4, RLVECT_2:19;

hence K . w = 0 by A3, FUNCT_1:47; :: thesis: verum

end;A4: w is VECTOR of V by RLSUB_1:10;

assume not w in C ; :: thesis: K . w = 0

then L . w = 0 by A4, RLVECT_2:19;

hence K . w = 0 by A3, FUNCT_1:47; :: thesis: verum

take K ; :: thesis: ( Carrier K = Carrier L & Sum K = Sum L )

thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th10; :: thesis: verum