let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U
for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
let f be Function of B,V; :: thesis: for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
let l2 be Linear_Combination of rng f; :: thesis: ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
defpred S₁[ object , object ] means ( ( $1 in B & $2 = l2 . (f . $1) ) or ( not $1 in B & $2 = 0. F ) );
B4: for x being object st x in the carrier of U holds
ex y being object st
( y in the carrier of F & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of U implies ex y being object st
( y in the carrier of F & S₁[x,y] ) )
assume x in the carrier of U ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

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

suppose S: x in B ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

then x in dom f by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:3;
then reconsider v = f . x as Element of V ;
l2 . v is Element of F ;
hence ex y being object st
( y in the carrier of F & S₁[x,y] ) by S; :: thesis: verum

end;

suppose not x in B ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

hence ex y being object st
( y in the carrier of F & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

consider l1 being Function of the carrier of U, the carrier of F such that
B5: for x being object st x in the carrier of U holds
S₁[x,l1 . x] from FUNCT_2:sch 1(B4);
reconsider l1 = l1 as Element of Funcs ( the carrier of U, the carrier of F) by FUNCT_2:8;
for u being Element of U st not u in B holds
l1 . u = 0. F by B5;
then reconsider l1 = l1 as Linear_Combination of U by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier l1 holds
o in B

let o be object ; :: thesis: ( o in Carrier l1 implies o in B )
assume o in Carrier l1 ; :: thesis: o in B
then consider v being Element of U such that
C1: ( o = v & l1 . v <> 0. F ) ;
thus o in B by C1, B5; :: thesis: verum

end;

then Carrier l1 c= B ;
then reconsider l1 = l1 as Linear_Combination of B by VECTSP_6:def 4;
take l1 ; :: thesis: for u being Element of U st u in B holds
l1 . u = l2 . (f . u)
thus for u being Element of U st u in B holds
l1 . u = l2 . (f . u) by B5; :: thesis: verum