let GF be Field; :: thesis: for V being VectSp of GF
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 V be VectSp of GF; :: 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 S1[ object , object ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0. GF ) );
reconsider K9 = K as Function of the carrier of W, the carrier of GF ;
A1: the carrier of W c= the carrier of V by VECTSP_4: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 the carrier of GF & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of GF & S1[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of GF & S1[x,y] )
then reconsider x = x as Vector of V ;
per cases ( x in W or not x in W ) ;
suppose A3: x in W ; :: thesis: ex y being object st
( y in the carrier of GF & S1[x,y] )
then reconsider x = x as Vector of W by STRUCT_0:def 5;
S1[x,K . x] by A3;
hence ex y being object st
( y in the carrier of GF & S1[x,y] ) ; :: thesis: verum
end;
suppose not x in W ; :: thesis: ex y being object st
( y in the carrier of GF & S1[x,y] )
hence ex y being object st
( y in the carrier of GF & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
ex L being Function of the carrier of V, the carrier of GF st
for x being object st x in the carrier of V holds
S1[x,L . x] from FUNCT_2:sch 1(A2);
 then consider L being Function of the carrier of V, the carrier of GF such that
A4: for x being object st x in the carrier of V holds
S1[x,L . x] ;
A5: now :: thesis: for v being Vector of V st not v in C holds
L . v = 0. GF
let v be Vector of V; :: thesis: ( not v in C implies L . v = 0. GF )
assume not v in C ; :: thesis: L . v = 0. GF
then ( ( S1[v,K . v] & not v in C & v in the carrier of W ) or S1[v, 0. GF] ) by STRUCT_0:def 5;
then ( ( S1[v,K . v] & K . v = 0. GF ) or S1[v, 0. GF] ) by VECTSP_6:2;
hence L . v = 0. GF by A4; :: thesis: verum
end;
L is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by A5, VECTSP_6:def 1;
reconsider L9 = L | the carrier of W as Function of the carrier of W, the carrier of GF 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
let x be object ; :: thesis: ( x in Carrier L implies x in the carrier of W )
assume that
A6: x in Carrier L and
A7: not x in the carrier of W ; :: thesis: contradiction
consider v being Vector of V such that
A8: x = v and
A9: L . v <> 0. GF by A6, VECTSP_6:1;
S1[v, 0. GF] by A7, A8, STRUCT_0:def 5;
hence contradiction by A4, A9; :: thesis: verum
end;
then A10: Carrier L c= the carrier of W ;
now :: thesis: for x being object st x in the carrier of W holds
K9 . x = L9 . x
let x be object ; :: thesis: ( x in the carrier of W implies K9 . x = L9 . x )
assume A11: x in the carrier of W ; :: thesis: K9 . x = L9 . x
then S1[x,L . x] by A4, A1;
hence K9 . x = L9 . x by A11, FUNCT_1:49, STRUCT_0:def 5; :: thesis: verum
end;
then K9 = L9 by FUNCT_2:12;
hence ( Carrier K = Carrier L & Sum K = Sum L ) by A10, Th7; :: thesis: verum