let R be non degenerated commutative Ring; :: thesis: for n being Nat
for o being Element of (R ^* n) ex l being Linear_Combination of Base (R,n) st Sum l = o
let n be Nat; :: thesis: for o being Element of (R ^* n) ex l being Linear_Combination of Base (R,n) st Sum l = o
let o be Element of (R ^* n); :: thesis: ex l being Linear_Combination of Base (R,n) st Sum l = o
o in the carrier of (R ^* n) ;
then H: o in n -tuples_on the carrier of R by DEF;
then reconsider t = o as Tuple of n, the carrier of R by FINSEQ_2:131;
defpred S₁[ object , object ] means ( ex i being Nat st
( 1 <= i & i <= n & $1 = i _th_unit_vector (n,R) & $2 = t . i ) or ( not $1 in Base (R,n) & $2 = 0. R ) );

A: now :: thesis: for x being object st x in the carrier of (R ^* n) holds
ex y being object st
( y in the carrier of R & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of (R ^* n) implies ex y being object st
( b₂ in the carrier of R & S₁[y,b₂] ) )
assume x in the carrier of (R ^* n) ; :: thesis: ex y being object st
( b₂ in the carrier of R & S₁[y,b₂] )

per cases ( x in Base (R,n) or not x in Base (R,n) ) ;

suppose x in Base (R,n) ; :: thesis: ex y being object st
( b₂ in the carrier of R & S₁[y,b₂] )

then consider i being Nat such that
B: ( x = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
i in Seg n by B;
then i in dom t by FINSEQ_2:124;
then t . i in rng t by FUNCT_1:3;
hence ex y being object st
( y in the carrier of R & S₁[x,y] ) by B; :: thesis: verum

end;

suppose not x in Base (R,n) ; :: thesis: ex y being object st
( b₂ in the carrier of R & S₁[y,b₂] )

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

end;

end;

end;

consider f being Function of the carrier of (R ^* n), the carrier of R such that
B: for x being object st x in the carrier of (R ^* n) holds
S₁[x,f . x] from FUNCT_2:sch 1(A);

D: now :: thesis: for v being Element of (R ^* n) st not v in Base (R,n) holds
f . v = 0. R

let v be Element of (R ^* n); :: thesis: ( not v in Base (R,n) implies f . v = 0. R )
assume E: not v in Base (R,n) ; :: thesis: f . v = 0. R
S₁[v,f . v] by B;
hence f . v = 0. R by E; :: thesis: verum

end;

( dom f = the carrier of (R ^* n) & rng f c= the carrier of R ) by FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (R ^* n), the carrier of R) by FUNCT_2:def 2;
ex T being finite Subset of (R ^* n) st
for v being Element of (R ^* n) st not v in T holds
f . v = 0. R

proof

take T = Base (R,n); :: thesis: for v being Element of (R ^* n) st not v in T holds
f . v = 0. R

now :: thesis: for v being Element of (R ^* n) st not v in T holds
f . v = 0. R

let v be Element of (R ^* n); :: thesis: ( not v in T implies f . v = 0. R )
assume E: not v in T ; :: thesis: f . v = 0. R
S₁[v,f . v] by B;
hence f . v = 0. R by E; :: thesis: verum

end;

hence for v being Element of (R ^* n) st not v in T holds
f . v = 0. R ; :: thesis: verum

end;

then reconsider l = f as Linear_Combination of R ^* n by VECTSP_6:def 1;
Carrier l c= Base (R,n)

proof

now :: thesis: for o being object st o in Carrier l holds
o in Base (R,n)

let o be object ; :: thesis: ( o in Carrier l implies o in Base (R,n) )
assume o in Carrier l ; :: thesis: o in Base (R,n)
then consider v being Element of (R ^* n) such that
E: ( o = v & l . v <> 0. R ) ;
thus o in Base (R,n) by D, E; :: thesis: verum

end;

hence Carrier l c= Base (R,n) ; :: thesis: verum

end;

then reconsider l = l as Linear_Combination of Base (R,n) by VECTSP_6:def 4;
Sum l in the carrier of (R ^* n) ;
then J: Sum l in n -tuples_on the carrier of R by DEF;
n -tuples_on the carrier of R = { s where s is Element of the carrier of R * : len s = n } by FINSEQ_2:def 4;
then consider s being Element of the carrier of R * such that
K: ( Sum l = s & len s = n ) by J;
reconsider u = Sum l as Tuple of n, the carrier of R by K, J;

E: now :: thesis: for i being Nat st 1 <= i & i <= n holds
u . i = t . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies u . i = t . i )
assume E1: ( 1 <= i & i <= n ) ; :: thesis: u . i = t . i
the carrier of (R ^* n) = n -tuples_on the carrier of R by DEF;
then S₁[i _th_unit_vector (n,R),l . (i _th_unit_vector (n,R))] by B;
then consider j being Nat such that
E2: ( 1 <= j & j <= n & j _th_unit_vector (n,R) = i _th_unit_vector (n,R) & l . (j _th_unit_vector (n,R)) = t . j ) by E1;
l . (i _th_unit_vector (n,R)) = t . i by E1, E2, u2;
hence u . i = t . i by E1, lemBase; :: thesis: verum

end;

( len u = n & len t = n ) by H, J, FINSEQ_2:133;
hence ex l being Linear_Combination of Base (R,n) st Sum l = o by E, FINSEQ_1:14; :: thesis: verum