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

for K being Linear_Combination of W ex L being Linear_Combination of V st

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

let W be Subspace of V; :: thesis: for K being Linear_Combination of W ex L being Linear_Combination of V st

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

let K be Linear_Combination of W; :: thesis: ex L being Linear_Combination of V st

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

defpred S_{1}[ object , object ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0 ) );

reconsider K9 = K as Function of the carrier of W,REAL ;

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

then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;

A2: for x being object st x in the carrier of V holds

ex y being object st

( y in REAL & S_{1}[x,y] )

for x being object st x in the carrier of V holds

S_{1}[x,L . x]
from FUNCT_2:sch 1(A2);

then consider L being Function of the carrier of V,REAL such that

A5: for x being object st x in the carrier of V holds

S_{1}[x,L . x]
;

then reconsider L = L as Linear_Combination of V by A6, RLVECT_2:def 3;

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

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

hence ( Carrier K = Carrier L & Sum K = Sum L ) by A11, Th10; :: thesis: verum

for K being Linear_Combination of W ex L being Linear_Combination of V st

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

let W be Subspace of V; :: thesis: for K being Linear_Combination of W ex L being Linear_Combination of V st

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

let K be Linear_Combination of W; :: thesis: ex L being Linear_Combination of V st

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

defpred S

reconsider K9 = K as Function of the carrier of W,REAL ;

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

then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;

A2: for x being object st x in the carrier of V holds

ex y being object st

( y in REAL & S

proof

ex L being Function of the carrier of V,REAL st
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in REAL & S_{1}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in REAL & S_{1}[x,y] )

then reconsider x = x as VECTOR of V ;

A3: 0 in REAL by XREAL_0:def 1;

end;( y in REAL & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in REAL & S

then reconsider x = x as VECTOR of V ;

A3: 0 in REAL by XREAL_0:def 1;

per cases
( x in W or not x in W )
;

end;

suppose A4:
x in W
; :: thesis: ex y being object st

( y in REAL & S_{1}[x,y] )

( y in REAL & S

then reconsider x = x as VECTOR of W by STRUCT_0:def 5;

S_{1}[x,K . x]
by A4;

hence ex y being object st

( y in REAL & S_{1}[x,y] )
; :: thesis: verum

end;S

hence ex y being object st

( y in REAL & S

for x being object st x in the carrier of V holds

S

then consider L being Function of the carrier of V,REAL such that

A5: for x being object st x in the carrier of V holds

S

A6: now :: thesis: for v being VECTOR of V st not v in C holds

L . v = 0

L is Element of Funcs ( the carrier of V,REAL)
by FUNCT_2:8;L . v = 0

let v be VECTOR of V; :: thesis: ( not v in C implies L . v = 0 )

assume not v in C ; :: thesis: L . v = 0

then ( ( S_{1}[v,K . v] & not v in C & v in the carrier of W ) or S_{1}[v, 0 ] )
by STRUCT_0:def 5;

then ( ( S_{1}[v,K . v] & K . v = 0 ) or S_{1}[v, 0 ] )
by RLVECT_2:19;

hence L . v = 0 by A5; :: thesis: verum

end;assume not v in C ; :: thesis: L . v = 0

then ( ( S

then ( ( S

hence L . v = 0 by A5; :: thesis: verum

then reconsider L = L as Linear_Combination of V by A6, RLVECT_2:def 3;

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

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

now :: thesis: for x being object st x in Carrier L holds

x in the carrier of W

then A11:
Carrier L c= the carrier of W
;x in the carrier of W

let x be object ; :: thesis: ( x in Carrier L implies x in the carrier of W )

assume that

A7: x in Carrier L and

A8: not x in the carrier of W ; :: thesis: contradiction

consider v being VECTOR of V such that

A9: x = v and

A10: L . v <> 0 by A7, Th3;

S_{1}[v, 0 ]
by A8, A9, STRUCT_0:def 5;

hence contradiction by A5, A10; :: thesis: verum

end;assume that

A7: x in Carrier L and

A8: not x in the carrier of W ; :: thesis: contradiction

consider v being VECTOR of V such that

A9: x = v and

A10: L . v <> 0 by A7, Th3;

S

hence contradiction by A5, A10; :: thesis: verum

now :: thesis: for x being object st x in the carrier of W holds

K9 . x = L9 . x

then
K9 = L9
by FUNCT_2:12;K9 . x = L9 . x

let x be object ; :: thesis: ( x in the carrier of W implies K9 . x = L9 . x )

assume A12: x in the carrier of W ; :: thesis: K9 . x = L9 . x

then S_{1}[x,L . x]
by A5, A1;

hence K9 . x = L9 . x by A12, FUNCT_1:49, STRUCT_0:def 5; :: thesis: verum

end;assume A12: x in the carrier of W ; :: thesis: K9 . x = L9 . x

then S

hence K9 . x = L9 . x by A12, FUNCT_1:49, STRUCT_0:def 5; :: thesis: verum

hence ( Carrier K = Carrier L & Sum K = Sum L ) by A11, Th10; :: thesis: verum