let n be Nat; :: thesis: for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)
let x0 be Element of REAL n; :: thesis: x0 = Sum (ProjFinSeq x0)
set f = ProjFinSeq x0;
reconsider n2 = n as Element of NAT by ORDINAL1:def 13;
now
per cases ( len (ProjFinSeq x0) > 0 or len (ProjFinSeq x0) <= 0 ) ;
case A1: len (ProjFinSeq x0) > 0 ; :: thesis: ( ( len (ProjFinSeq x0) > 0 implies ex g being FinSequence of REAL n st
( len (ProjFinSeq x0) = len g & (ProjFinSeq x0) . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len (ProjFinSeq x0) holds
g . (i + 1) = (g /. i) + ((ProjFinSeq x0) /. (i + 1)) ) & x0 = g . (len (ProjFinSeq x0)) ) ) & ( len (ProjFinSeq x0) <= 0 implies x0 = 0* n ) )
then consider g2 being FinSequence of REAL n such that
A2: len (ProjFinSeq x0) = len g2 and
A3: (ProjFinSeq x0) . 1 = g2 . 1 and
A4: for i being Nat st 1 <= i & i < len (ProjFinSeq x0) holds
g2 . (i + 1) = (g2 /. i) + ((ProjFinSeq x0) /. (i + 1)) and
Sum (ProjFinSeq x0) = g2 . (len (ProjFinSeq x0)) by Def10;
defpred S1[ Nat] means for i being Nat st 1 <= i & i <= len (ProjFinSeq x0) & 1 <= $1 & $1 <= len (ProjFinSeq x0) holds
( ( i <= $1 implies (g2 /. $1) . i = x0 . i ) & ( i > $1 implies (g2 /. $1) . i = 0 ) );
A5: len (ProjFinSeq x0) = n by Def12;
A6: 0 + 1 <= len (ProjFinSeq x0) by A1, NAT_1:13;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
reconsider k2 = k as Element of NAT by ORDINAL1:def 13;
assume A8: S1[k] ; :: thesis: S1[k + 1]
for i being Nat st 1 <= i & i <= len (ProjFinSeq x0) & 1 <= k + 1 & k + 1 <= len (ProjFinSeq x0) holds
( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) )
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (ProjFinSeq x0) & 1 <= k + 1 & k + 1 <= len (ProjFinSeq x0) implies ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) ) )
assume that
A9: 1 <= i and
A10: i <= len (ProjFinSeq x0) and
A11: 1 <= k + 1 and
A12: k + 1 <= len (ProjFinSeq x0) ; :: thesis: ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) )
g2 /. (k + 1) is Element of REAL n ;
then reconsider r = g2 . (k + 1) as Element of REAL n by A2, A11, A12, FINSEQ_4:24;
reconsider i2 = i as Element of NAT by ORDINAL1:def 13;
A13: g2 /. (k + 1) = g2 . (k + 1) by A2, A11, A12, FINSEQ_4:24;
now
per cases ( 1 <= k or k < 1 ) ;
case A14: 1 <= k ; :: thesis: ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) )
reconsider r3 = (ProjFinSeq x0) /. (k + 1) as Element of REAL n ;
reconsider r2 = g2 /. k as Element of REAL n ;
A15: (ProjFinSeq x0) /. (k + 1) = (ProjFinSeq x0) . (k + 1) by A11, A12, FINSEQ_4:24
.= |(x0,(Base_FinSeq n2,(k + 1)))| * (Base_FinSeq n2,(k + 1)) by A5, A11, A12, Def12 ;
A16: k < k + 1 by XREAL_1:31;
then A17: k < len (ProjFinSeq x0) by A12, XXREAL_0:2;
then r = (g2 /. k) + ((ProjFinSeq x0) /. (k + 1)) by A4, A14;
then A18: r . i = (r2 . i) + (r3 . i) by RVSUM_1:27;
A19: now
assume A20: i <= k + 1 ; :: thesis: (g2 /. (k + 1)) . i = x0 . i
per cases ( i < k + 1 or i = k + 1 ) by A20, XXREAL_0:1;
suppose A21: i < k + 1 ; :: thesis: (g2 /. (k + 1)) . i = x0 . i
then A22: i <= k by NAT_1:13;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 0 by A5, A9, A10, A21, MATRIXR2:76 ;
hence (g2 /. (k + 1)) . i = x0 . i by A8, A9, A10, A13, A14, A17, A18, A22; :: thesis: verum
end;
suppose A23: i = k + 1 ; :: thesis: (g2 /. (k + 1)) . i = x0 . i
then A24: (g2 /. k) . i = 0 by A8, A9, A10, A14, A16, A17;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 1 by A5, A9, A10, A23, MATRIXR2:75
.= x0 . (k + 1) by A5, A11, A12, Th32 ;
hence (g2 /. (k + 1)) . i = x0 . i by A2, A9, A10, A18, A23, A24, FINSEQ_4:24; :: thesis: verum
end;
end;
end;
now
assume A25: i > k + 1 ; :: thesis: (g2 /. (k + 1)) . i = 0
then A26: i > k by A16, XXREAL_0:2;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 0 by A5, A9, A10, A25, MATRIXR2:76
.= 0 ;
hence (g2 /. (k + 1)) . i = 0 by A8, A9, A10, A13, A14, A17, A18, A26; :: thesis: verum
end;
hence ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) ) by A19; :: thesis: verum
end;
case k < 1 ; :: thesis: ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) )
then A27: k + 1 <= 0 + 1 by NAT_1:13;
then A28: k = 0 by XREAL_1:8;
A29: now
assume A30: i > 0 + 1 ; :: thesis: (g2 /. (k + 1)) . i = 0
g2 /. 1 = (ProjFinSeq x0) . 1 by A6, A2, A3, FINSEQ_4:24;
then (g2 /. 1) . i = (|(x0,(Base_FinSeq n2,1))| * (Base_FinSeq n2,1)) . i by A6, A5, Def12
.= |(x0,(Base_FinSeq n2,1))| * ((Base_FinSeq n2,1) . i2) by RVSUM_1:66
.= |(x0,(Base_FinSeq n2,1))| * 0 by A5, A10, A30, MATRIXR2:76
.= 0 ;
hence (g2 /. (k + 1)) . i = 0 by A28; :: thesis: verum
end;
A31: now
assume i <= 0 + 1 ; :: thesis: (g2 /. (0 + 1)) . i = x0 . i
then A32: i = 1 by A9, XXREAL_0:1;
g2 /. 1 = (ProjFinSeq x0) . 1 by A6, A2, A3, FINSEQ_4:24;
then (g2 /. 1) . 1 = (|(x0,(Base_FinSeq n2,1))| * (Base_FinSeq n2,1)) . 1 by A6, A5, Def12
.= |(x0,(Base_FinSeq n2,1))| * ((Base_FinSeq n2,1) . 1) by RVSUM_1:66
.= |(x0,(Base_FinSeq n2,1))| * 1 by A6, A5, MATRIXR2:75
.= x0 . 1 by A6, A5, Th32 ;
hence (g2 /. (0 + 1)) . i = x0 . i by A32; :: thesis: verum
end;
k <= 0 by A27, XREAL_1:8;
hence ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) ) by A31, A29; :: thesis: verum
end;
end;
end;
hence ( ( i <= k + 1 implies (g2 /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies (g2 /. (k + 1)) . i = 0 ) ) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider r4 = g2 /. (len (ProjFinSeq x0)) as Element of REAL n ;
A33: len x0 = n by FINSEQ_1:def 18;
then A34: len x0 = len r4 by FINSEQ_1:def 18;
A35: S1[ 0 ] ;
A36: for k being Nat holds S1[k] from NAT_1:sch 2(A35, A7);
 for i being Nat st 1 <= i & i <= len r4 holds
(g2 /. (len (ProjFinSeq x0))) . i = x0 . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len r4 implies (g2 /. (len (ProjFinSeq x0))) . i = x0 . i )
assume that
A37: 1 <= i and
A38: i <= len r4 ; :: thesis: (g2 /. (len (ProjFinSeq x0))) . i = x0 . i
A39: i <= len (ProjFinSeq x0) by A5, A38, FINSEQ_1:def 18;
1 <= len (ProjFinSeq x0) by A5, A33, A34, A37, A38, XXREAL_0:2;
hence (g2 /. (len (ProjFinSeq x0))) . i = x0 . i by A36, A37, A39; :: thesis: verum
end;
then x0 = g2 /. (len (ProjFinSeq x0)) by A34, FINSEQ_1:18;
then x0 = g2 . (len (ProjFinSeq x0)) by A6, A2, FINSEQ_4:24;
hence ( ( len (ProjFinSeq x0) > 0 implies ex g being FinSequence of REAL n st
( len (ProjFinSeq x0) = len g & (ProjFinSeq x0) . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len (ProjFinSeq x0) holds
g . (i + 1) = (g /. i) + ((ProjFinSeq x0) /. (i + 1)) ) & x0 = g . (len (ProjFinSeq x0)) ) ) & ( len (ProjFinSeq x0) <= 0 implies x0 = 0* n ) ) by A1, A2, A3, A4; :: thesis: verum
end;
case A40: len (ProjFinSeq x0) <= 0 ; :: thesis: ( ( len (ProjFinSeq x0) > 0 implies ex g being FinSequence of REAL n st
( len (ProjFinSeq x0) = len g & (ProjFinSeq x0) . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len (ProjFinSeq x0) holds
g . (i + 1) = (g /. i) + ((ProjFinSeq x0) /. (i + 1)) ) & x0 = g . (len (ProjFinSeq x0)) ) ) & ( len (ProjFinSeq x0) <= 0 implies x0 = 0* n ) )
then A41: n = 0 by Def12;
then x0 = <*> REAL ;
hence ( ( len (ProjFinSeq x0) > 0 implies ex g being FinSequence of REAL n st
( len (ProjFinSeq x0) = len g & (ProjFinSeq x0) . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len (ProjFinSeq x0) holds
g . (i + 1) = (g /. i) + ((ProjFinSeq x0) /. (i + 1)) ) & x0 = g . (len (ProjFinSeq x0)) ) ) & ( len (ProjFinSeq x0) <= 0 implies x0 = 0* n ) ) by A40, A41; :: thesis: verum
end;
end;
end;
hence x0 = Sum (ProjFinSeq x0) by Def10; :: thesis: verum