defpred S₁[ object , object ] means ( ex u being Element of B st
( $1 = f . u & $2 = Sum (Expand (f,l,(f . u))) ) or ( ( for u being Element of B holds not $1 = f . u ) & $2 = 0. F ) );
A1: for x being object st x in the carrier of V 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 V implies ex y being object st
( y in the carrier of F & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )
then reconsider x = x as Element of V ;

per cases ( ex w being Element of B st x = f . w or for w being Element of B holds not x = f . w ) ;

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

then consider w being Element of B such that
B: x = f . w ;
take Sum (Expand (f,l,(f . w))) ; :: thesis: ( Sum (Expand (f,l,(f . w))) in the carrier of F & S₁[x, Sum (Expand (f,l,(f . w)))] )
thus ( Sum (Expand (f,l,(f . w))) in the carrier of F & S₁[x, Sum (Expand (f,l,(f . w)))] ) by B; :: thesis: verum

end;

suppose B: for w being Element of B holds not x = f . w ; :: thesis: ex y being object st
( y in the carrier of F & S₁[x,y] )

take 0. F ; :: thesis: ( 0. F in the carrier of F & S₁[x, 0. F] )
thus ( 0. F in the carrier of F & S₁[x, 0. F] ) by B; :: thesis: verum

end;

end;

end;

consider g being Function of the carrier of V, the carrier of F such that
A2: for x being object st x in the carrier of V holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
H: dom f = B by FUNCT_2:def 1;
A7: for w being Element of V holds g . w = Sum (Expand (f,l,w))

proof

let w be Element of V; :: thesis: g . w = Sum (Expand (f,l,w))

per cases ( ex x being Element of B st w = f . x or for x being Element of B holds not w = f . x ) ;

suppose B0: ex x being Element of B st w = f . x ; :: thesis: g . w = Sum (Expand (f,l,w))

S₁[w,g . w] by A2;
hence g . w = Sum (Expand (f,l,w)) by B0; :: thesis: verum

end;

suppose for x being Element of B holds not w = f . x ; :: thesis: g . w = Sum (Expand (f,l,w))

then for x being object holds
( not x in dom f or not w = f . x ) ;
then B1: not w in rng f by FUNCT_1:def 3;

now :: thesis: for o being object holds not o in {w} /\ (rng f)

let o be object ; :: thesis: not o in {w} /\ (rng f)
assume o in {w} /\ (rng f) ; :: thesis: contradiction
then ( o in {w} & o in rng f ) by XBOOLE_0:def 4;
hence contradiction by B1, TARSKI:def 1; :: thesis: verum

end;

then {w} misses rng f by XBOOLE_0:def 1;
then f " {w} = {} by RELAT_1:138;
then B2: Expand (f,l,w) = <*> the carrier of F ;
S₁[w,g . w] by A2;
hence g . w = Sum (Expand (f,l,w)) by B2, RLVECT_1:43; :: thesis: verum

end;

end;

end;

reconsider g = g as Element of Funcs ( the carrier of V, the carrier of F) by FUNCT_2:8;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
g . v = 0. F

proof

reconsider T = rng f as finite Subset of V ;
take T ; :: thesis: for v being Element of V st not v in T holds
g . v = 0. F

now :: thesis: for v being Element of V st not v in T holds
g . v = 0. F

let v be Element of V; :: thesis: ( not v in T implies g . v = 0. F )
B0: S₁[v,g . v] by A2;
assume not v in T ; :: thesis: g . v = 0. F
hence g . v = 0. F by B0, H, FUNCT_1:def 3; :: thesis: verum

end;

hence for v being Element of V st not v in T holds
g . v = 0. F ; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of V by VECTSP_6:def 1;
Carrier g c= rng f

proof

now :: thesis: for o being object st o in Carrier g holds
o in rng f

let o be object ; :: thesis: ( o in Carrier g implies o in rng f )
assume o in Carrier g ; :: thesis: o in rng f
then consider v being Element of V such that
B0: ( o = v & g . v <> 0. F ) ;
consider u being Element of B such that
B1: ( v = f . u & g . v = Sum (Expand (f,l,(f . u))) ) by B0, A2;
dom f = B by FUNCT_2:def 1;
hence o in rng f by B0, B1, FUNCT_1:3; :: thesis: verum

end;

hence Carrier g c= rng f ; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of rng f by VECTSP_6:def 4;
take g ; :: thesis: for v being Element of V holds g . v = Sum (Expand (f,l,v))
thus for v being Element of V holds g . v = Sum (Expand (f,l,v)) by A7; :: thesis: verum