let R be non degenerated commutative Ring; :: thesis: for n being Nat
for l being Linear_Combination of Base (R,n)
for v being Tuple of n, the carrier of R
for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))
let n be Nat; :: thesis: for l being Linear_Combination of Base (R,n)
for v being Tuple of n, the carrier of R
for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))
let l be Linear_Combination of Base (R,n); :: thesis: for v being Tuple of n, the carrier of R
for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))
let v be Tuple of n, the carrier of R; :: thesis: for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))
let i be Nat; :: thesis: ( v = Sum l & 1 <= i & i <= n implies v . i = l . (i _th_unit_vector (n,R)) )
assume AS: ( v = Sum l & 1 <= i & i <= n ) ; :: thesis: v . i = l . (i _th_unit_vector (n,R))
set V = R ^* n;
set B = Base (R,n);
consider F being FinSequence of the carrier of (R ^* n) such that
A1: ( F is one-to-one & rng F = Carrier l & Sum l = Sum (l (#) F) ) by VECTSP_6:def 6;
set H = l (#) F;
A2: ( len (l (#) F) = len F & ( for i being Nat st i in dom (l (#) F) holds
(l (#) F) . i = (l . (F /. i)) * (F /. i) ) ) by VECTSP_6:def 5;

per cases ( l (#) F = {} or l (#) F <> {} ) ;

suppose l (#) F = {} ; :: thesis: v . i = l . (i _th_unit_vector (n,R))

then B3: F = {} by VECTSP_6:def 5;
then Carrier l = {} by A1;
then l = ZeroLC (R ^* n) by VECTSP_6:def 3;
then Sum l = 0. (R ^* n) by VECTSP_6:15
.= n |-> (0. R) by DEF ;
then B4: v . i = ((Seg n) --> (0. R)) . i by AS, FINSEQ_2:def 2
.= 0. R by AS, FINSEQ_1:1, FUNCOP_1:7 ;
the carrier of (R ^* n) = n -tuples_on the carrier of R by DEF;
hence v . i = l . (i _th_unit_vector (n,R)) by A1, B4, B3, VECTSP_6:2; :: thesis: verum

end;

suppose Y1: l (#) F <> {} ; :: thesis: v . i = l . (i _th_unit_vector (n,R))

then len (l (#) F) > 0 ;
then 0 + 1 <= len (l (#) F) by INT_1:7;
then Y2: 1 in dom F by A2, FINSEQ_3:25;
defpred S₁[ Nat] means for v being Tuple of n, the carrier of R st $1 <= len (l (#) F) & v = Sum ((l (#) F) | $1) holds
for m being Nat st 1 <= m & m <= n & not ( m _th_unit_vector (n,R) in rng (F | $1) & v . m = l . (m _th_unit_vector (n,R)) ) holds
( not m _th_unit_vector (n,R) in rng (F | $1) & v . m = 0. R );
IA: S₁[1]

proof

now :: thesis: for v being Tuple of n, the carrier of R st 1 <= len (l (#) F) & v = Sum ((l (#) F) | 1) holds
for m being Nat st 1 <= m & m <= n & not ( m _th_unit_vector (n,R) in rng (F | 1) & v . m = l . (m _th_unit_vector (n,R)) ) holds
( not m _th_unit_vector (n,R) in rng (F | 1) & v . m = 0. R )

let v be Tuple of n, the carrier of R; :: thesis: ( 1 <= len (l (#) F) & v = Sum ((l (#) F) | 1) implies for m being Nat st 1 <= m & m <= n & not ( b₃ _th_unit_vector (n,R) in rng (F | 1) & b₂ . b₃ = l . (b₃ _th_unit_vector (n,R)) ) holds
( not b₃ _th_unit_vector (n,R) in rng (F | 1) & b₂ . b₃ = 0. R ) )
assume C1: ( 1 <= len (l (#) F) & v = Sum ((l (#) F) | 1) ) ; :: thesis: for m being Nat st 1 <= m & m <= n & not ( b₃ _th_unit_vector (n,R) in rng (F | 1) & b₂ . b₃ = l . (b₃ _th_unit_vector (n,R)) ) holds
( not b₃ _th_unit_vector (n,R) in rng (F | 1) & b₂ . b₃ = 0. R )
let m be Nat; :: thesis: ( 1 <= m & m <= n & not ( b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) implies ( not b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = 0. R ) )
assume C2: ( 1 <= m & m <= n ) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = 0. R ) )
C5: dom ((l (#) F) | (Seg 1)) c= dom (l (#) F) by RELAT_1:60;
C3: (l (#) F) | 1 = <*(((l (#) F) | 1) . 1)*> by C1, FINSEQ_1:59, FINSEQ_1:40;
then dom ((l (#) F) | 1) = {1} by FINSEQ_1:2, FINSEQ_1:38;
then C6: 1 in dom ((l (#) F) | 1) by TARSKI:def 1;
then ((l (#) F) | 1) . 1 = ((l (#) F) | 1) /. 1 by PARTFUN1:def 6;
then C9: Sum ((l (#) F) | 1) = ((l (#) F) | 1) . 1 by C3, RLVECT_1:44
.= (l (#) F) . 1 by C6, FUNCT_1:47
.= (l . (F /. 1)) * (F /. 1) by C5, C6, VECTSP_6:def 5 ;
rng F c= Base (R,n) by A1, VECTSP_6:def 4;
then F . 1 in Base (R,n) by Y2, FUNCT_1:3;
then consider i being Nat such that
C7: ( F . 1 = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
C8: v = (l . (F /. 1)) * (i _th_unit_vector (n,R)) by C1, C7, C9, Y2, PARTFUN1:def 6, lemBB;

per cases ( m = i or m <> i ) ;

suppose D1: m = i ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = 0. R ) )

D2: 1 in Seg 1 ;
F /. 1 = i _th_unit_vector (n,R) by C7, Y2, PARTFUN1:def 6;
hence ( ( m _th_unit_vector (n,R) in rng (F | 1) & v . m = l . (m _th_unit_vector (n,R)) ) or ( not m _th_unit_vector (n,R) in rng (F | 1) & v . m = 0. R ) ) by D1, D2, C8, C7, Y2, FUNCT_1:50, lemBA; :: thesis: verum

end;

suppose D0: m <> i ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | 1) & b₁ . b₂ = 0. R ) )

then D1: m _th_unit_vector (n,R) <> i _th_unit_vector (n,R) by C2, C7, u2;

now :: thesis: not m _th_unit_vector (n,R) in rng (F | 1)

assume m _th_unit_vector (n,R) in rng (F | 1) ; :: thesis: contradiction
then consider x being object such that
D2: ( x in dom (F | 1) & (F | 1) . x = m _th_unit_vector (n,R) ) by FUNCT_1:def 3;
D3: (F | 1) . x = F . x by D2, FUNCT_1:47;
F | 1 = <*((F | 1) . 1)*> by A2, C1, FINSEQ_1:59, FINSEQ_1:40;
then dom (F | 1) = {1} by FINSEQ_1:2, FINSEQ_1:38;
hence contradiction by C7, D1, D2, D3, TARSKI:def 1; :: thesis: verum

end;

hence ( ( m _th_unit_vector (n,R) in rng (F | 1) & v . m = l . (m _th_unit_vector (n,R)) ) or ( not m _th_unit_vector (n,R) in rng (F | 1) & v . m = 0. R ) ) by C2, C7, C8, D0, lemBA; :: thesis: verum

end;

end;

end;

hence S₁[1] ; :: thesis: verum

end;

IS: now :: thesis: for k being Element of NAT st 1 <= k & k < len (l (#) F) & S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis: ( 1 <= k & k < len (l (#) F) & S₁[k] implies S₁[k + 1] )
assume AS: ( 1 <= k & k < len (l (#) F) ) ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for v being Tuple of n, the carrier of R st k + 1 <= len (l (#) F) & v = Sum ((l (#) F) | (k + 1)) holds
for m being Nat st 1 <= m & m <= n & not ( m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = l . (m _th_unit_vector (n,R)) ) holds
( not m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = 0. R )

let v be Tuple of n, the carrier of R; :: thesis: ( k + 1 <= len (l (#) F) & v = Sum ((l (#) F) | (k + 1)) implies for m being Nat st 1 <= m & m <= n & not ( b₃ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₂ . b₃ = l . (b₃ _th_unit_vector (n,R)) ) holds
( not b₃ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₂ . b₃ = 0. R ) )
assume C1: ( k + 1 <= len (l (#) F) & v = Sum ((l (#) F) | (k + 1)) ) ; :: thesis: for m being Nat st 1 <= m & m <= n & not ( b₃ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₂ . b₃ = l . (b₃ _th_unit_vector (n,R)) ) holds
( not b₃ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₂ . b₃ = 0. R )
let m be Nat; :: thesis: ( 1 <= m & m <= n & not ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) implies ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )
assume C2: ( 1 <= m & m <= n ) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )
set G1 = (l (#) F) | k;
reconsider v1 = Sum ((l (#) F) | k) as Element of n -tuples_on the carrier of R by DEF;
H: ( 1 <= k + 1 & k <= k + 1 ) by NAT_1:11;
then C3: k <= len (l (#) F) by C1, XXREAL_0:2;
C4: len ((l (#) F) | (k + 1)) = k + 1 by C1, FINSEQ_1:59;
((l (#) F) | (k + 1)) | (Seg k) = ((l (#) F) | (k + 1)) | k
.= (l (#) F) | k by NAT_1:11, FINSEQ_1:82 ;
then C5: (l (#) F) | (k + 1) = ((l (#) F) | k) ^ <*(((l (#) F) | (k + 1)) . (k + 1))*> by C1, FINSEQ_1:59, FINSEQ_3:55;
dom ((l (#) F) | (k + 1)) = Seg (k + 1) by C4, FINSEQ_1:def 3;
then C6: k + 1 in dom ((l (#) F) | (k + 1)) by H;
C7: dom ((l (#) F) | (k + 1)) c= dom (l (#) F) by RELAT_1:60;
((l (#) F) | (k + 1)) . (k + 1) = (l (#) F) . (k + 1) by C6, FUNCT_1:47
.= (l (#) F) /. (k + 1) by C6, C7, PARTFUN1:def 6 ;
then C8: Sum ((l (#) F) | (k + 1)) = (Sum ((l (#) F) | k)) + (Sum <*((l (#) F) /. (k + 1))*>) by C5, RLVECT_1:41
.= (Sum ((l (#) F) | k)) + ((l (#) F) /. (k + 1)) by RLVECT_1:44 ;
F | k = (F | (k + 1)) | k by NAT_1:11, FINSEQ_1:82;
then C9: rng (F | k) c= rng (F | (k + 1)) by RELAT_1:70;
E0: dom F = Seg (len (l (#) F)) by A2, FINSEQ_1:def 3
.= dom (l (#) F) by FINSEQ_1:def 3 ;
E1: rng F c= Base (R,n) by A1, VECTSP_6:def 4;
F . (k + 1) in Base (R,n) by E1, E0, C6, C7, FUNCT_1:3;
then consider i being Nat such that
E2: ( F . (k + 1) = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
E4: (l (#) F) /. (k + 1) = (l (#) F) . (k + 1) by C6, C7, PARTFUN1:def 6
.= (l . (F /. (k + 1))) * (F /. (k + 1)) by C7, C6, VECTSP_6:def 5
.= (l . (F /. (k + 1))) * (i _th_unit_vector (n,R)) by E0, C6, C7, E2, PARTFUN1:def 6, lemBB ;
E5: v = v1 + ((l . (F /. (k + 1))) * (i _th_unit_vector (n,R))) by C1, C8, E4, lemBC;
len (F | (k + 1)) = k + 1 by A2, C1, FINSEQ_1:59;
then dom (F | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then E6: k + 1 in dom (F | (k + 1)) by H;

per cases ( not m _th_unit_vector (n,R) in rng (F | (k + 1)) or m _th_unit_vector (n,R) in rng (F | (k + 1)) ) ;

suppose D0: not m _th_unit_vector (n,R) in rng (F | (k + 1)) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )

then not m _th_unit_vector (n,R) in rng (F | k) by C9;
then D1: v1 . m = 0. R by C2, C3, IV;
D4: m in Seg n by C2;

now :: thesis: not m _th_unit_vector (n,R) = i _th_unit_vector (n,R)

assume D5: m _th_unit_vector (n,R) = i _th_unit_vector (n,R) ; :: thesis: contradiction
(F | (k + 1)) . (k + 1) = i _th_unit_vector (n,R) by E2, E6, FUNCT_1:47;
hence contradiction by D0, D5, E6, FUNCT_1:def 3; :: thesis: verum

end;

then (i _th_unit_vector (n,R)) . m = 0. R by E2, C2, u1;
then ((l . (F /. (k + 1))) * (i _th_unit_vector (n,R))) . m = (l . (F /. (k + 1))) * (0. R) by D4, FVSUM_1:51;
then v . m = (0. R) + (0. R) by E5, D4, D1, FVSUM_1:18
.= 0. R ;
hence ( ( m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = l . (m _th_unit_vector (n,R)) ) or ( not m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = 0. R ) ) by D0; :: thesis: verum

end;

suppose D0: m _th_unit_vector (n,R) in rng (F | (k + 1)) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )

m _th_unit_vector (n,R) in n -tuples_on the carrier of R ;
then F1: ( dom l = the carrier of (R ^* n) & m _th_unit_vector (n,R) in the carrier of (R ^* n) ) by DEF, FUNCT_2:def 1;

per cases ( m _th_unit_vector (n,R) in rng (F | k) or not m _th_unit_vector (n,R) in rng (F | k) ) ;

suppose D7: m _th_unit_vector (n,R) in rng (F | k) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )

then D1: v1 . m = l . (m _th_unit_vector (n,R)) by C2, C3, IV
.= l /. (m _th_unit_vector (n,R)) by F1, PARTFUN1:def 6 ;
D4: m in Seg n by C2;
consider x being object such that
D5: ( x in dom (F | k) & (F | k) . x = m _th_unit_vector (n,R) ) by D7, FUNCT_1:def 3;
reconsider x = x as Element of NAT by D5;
len (F | k) = k by AS, A2, FINSEQ_1:59;
then dom (F | k) = Seg k by FINSEQ_1:def 3;
then ( 1 <= x & x <= k ) by D5, FINSEQ_1:1;
then D8: x + 0 < k + 1 by XREAL_1:8;
D9: dom (F | k) c= dom F by RELAT_1:60;
m _th_unit_vector (n,R) <> i _th_unit_vector (n,R)

proof

F . x = m _th_unit_vector (n,R) by D5, FUNCT_1:47;
hence m _th_unit_vector (n,R) <> i _th_unit_vector (n,R) by E0, E2, C6, C7, D8, D9, D5, A1; :: thesis: verum

end;

then (i _th_unit_vector (n,R)) . m = 0. R by E2, C2, u1;
then ((l . (F /. (k + 1))) * (i _th_unit_vector (n,R))) . m = (l . (F /. (k + 1))) * (0. R) by D4, FVSUM_1:51;
then v . m = (l /. (m _th_unit_vector (n,R))) + (0. R) by E5, D4, D1, FVSUM_1:18
.= l . (m _th_unit_vector (n,R)) by F1, PARTFUN1:def 6 ;
hence ( ( m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = l . (m _th_unit_vector (n,R)) ) or ( not m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = 0. R ) ) by D0; :: thesis: verum

end;

suppose D7: not m _th_unit_vector (n,R) in rng (F | k) ; :: thesis: ( ( b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = l . (b₂ _th_unit_vector (n,R)) ) or ( not b₂ _th_unit_vector (n,R) in rng (F | (k + 1)) & b₁ . b₂ = 0. R ) )

then D1: v1 . m = 0. R by C2, C3, IV;
D4: m in Seg n by C2;
consider x being object such that
D5: ( x in dom (F | (k + 1)) & (F | (k + 1)) . x = m _th_unit_vector (n,R) ) by D0, FUNCT_1:def 3;
reconsider x = x as Element of NAT by D5;
len (F | (k + 1)) = k + 1 by A2, C1, FINSEQ_1:59;
then D10: dom (F | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then D11: ( 1 <= x & x <= k + 1 ) by D5, FINSEQ_1:1;

D8: now :: thesis: not x <> k + 1

assume x <> k + 1 ; :: thesis: contradiction
then x < k + 1 by D11, XXREAL_0:1;
then ( 1 <= x & x <= k ) by D10, D5, FINSEQ_1:1, INT_1:7;
then E1: x in Seg k ;
len (F | k) = k by AS, A2, FINSEQ_1:59;
then E3: x in dom (F | k) by E1, FINSEQ_1:def 3;
(F | k) . x = F . x by E3, FUNCT_1:47
.= (F | (k + 1)) . x by D5, FUNCT_1:47 ;
hence contradiction by E3, D5, D7, FUNCT_1:3; :: thesis: verum

end;

D9: dom (F | (k + 1)) c= dom F by RELAT_1:60;
F . x = m _th_unit_vector (n,R) by D5, FUNCT_1:47;
then D12: F /. (k + 1) = m _th_unit_vector (n,R) by D5, D8, D9, PARTFUN1:def 6;
m _th_unit_vector (n,R) = i _th_unit_vector (n,R) by E2, D8, D5, FUNCT_1:47;
then (i _th_unit_vector (n,R)) . m = 1. R by C2, u1;
then ((l . (F /. (k + 1))) * (i _th_unit_vector (n,R))) . m = (l . (F /. (k + 1))) * (1. R) by D4, FVSUM_1:51
.= l /. (m _th_unit_vector (n,R)) by D12, F1, PARTFUN1:def 6 ;
then v . m = (0. R) + (l /. (m _th_unit_vector (n,R))) by E5, D4, D1, FVSUM_1:18
.= l . (m _th_unit_vector (n,R)) by F1, PARTFUN1:def 6 ;
hence ( ( m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = l . (m _th_unit_vector (n,R)) ) or ( not m _th_unit_vector (n,R) in rng (F | (k + 1)) & v . m = 0. R ) ) by D0; :: thesis: verum

end;

end;

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A3: for k being Element of NAT st 1 <= k & k <= len (l (#) F) holds
S₁[k] from INT_1:sch 7(IA, IS);
len (l (#) F) > 0 by Y1;
then A4: 0 + 1 <= len (l (#) F) by INT_1:7;
A5: v = Sum ((l (#) F) | (len (l (#) F))) by AS, A1, FINSEQ_1:58;
A6: F | (len (l (#) F)) = F by A2, FINSEQ_1:58;
H: the carrier of (R ^* n) = n -tuples_on the carrier of R by DEF;

per cases ( i _th_unit_vector (n,R) in Carrier l or not i _th_unit_vector (n,R) in Carrier l ) ;

suppose i _th_unit_vector (n,R) in Carrier l ; :: thesis: v . i = l . (i _th_unit_vector (n,R))

hence v . i = l . (i _th_unit_vector (n,R)) by AS, A1, A3, A4, A5, A6; :: thesis: verum

end;

suppose A7: not i _th_unit_vector (n,R) in Carrier l ; :: thesis: v . i = l . (i _th_unit_vector (n,R))

hence v . i = 0. R by AS, A1, A3, A4, A5, A6
.= l . (i _th_unit_vector (n,R)) by H, A7 ;
:: thesis: verum

end;

end;

end;

end;