let n be Nat; for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)
let x0 be Element of REAL n; x0 = Sum (ProjFinSeq x0)
set f = ProjFinSeq x0;
reconsider n2 = n as Element of NAT by ORDINAL1:def 12;
now ( ( len (ProjFinSeq x0) > 0 & x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0)) ) or ( len (ProjFinSeq x0) <= 0 & x0 = 0* n ) )per cases
( len (ProjFinSeq x0) > 0 or len (ProjFinSeq x0) <= 0 )
;
case A1:
len (ProjFinSeq x0) > 0
;
x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0))set g2 =
accum (ProjFinSeq x0);
A2:
len (ProjFinSeq x0) = len (accum (ProjFinSeq x0))
by Def10;
A3:
(ProjFinSeq x0) . 1
= (accum (ProjFinSeq x0)) . 1
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
((accum (ProjFinSeq x0)) /. $1) . i = x0 . i ) & (
i > $1 implies
((accum (ProjFinSeq x0)) /. $1) . i = 0 ) );
A4:
len (ProjFinSeq x0) = n
by Def12;
A5:
0 + 1
<= len (ProjFinSeq x0)
by A1, NAT_1:13;
A6:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider k2 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A7:
S1[
k]
;
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
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & (
i > k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
proof
let i be
Nat;
( 1 <= i & i <= len (ProjFinSeq x0) & 1 <= k + 1 & k + 1 <= len (ProjFinSeq x0) implies ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) )
assume that A8:
1
<= i
and A9:
i <= len (ProjFinSeq x0)
and A10:
1
<= k + 1
and A11:
k + 1
<= len (ProjFinSeq x0)
;
( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
(accum (ProjFinSeq x0)) /. (k + 1) is
Element of
REAL n
;
then reconsider r =
(accum (ProjFinSeq x0)) . (k + 1) as
Element of
REAL n by A2, A10, A11, FINSEQ_4:15;
reconsider i2 =
i as
Element of
NAT by ORDINAL1:def 12;
A12:
(accum (ProjFinSeq x0)) /. (k + 1) = (accum (ProjFinSeq x0)) . (k + 1)
by A2, A10, A11, FINSEQ_4:15;
now ( ( 1 <= k & ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) or ( k < 1 & ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) )per cases
( 1 <= k or k < 1 )
;
case A13:
1
<= k
;
( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )reconsider r3 =
(ProjFinSeq x0) /. (k + 1) as
Element of
REAL n ;
reconsider r2 =
(accum (ProjFinSeq x0)) /. k as
Element of
REAL n ;
A14:
(ProjFinSeq x0) /. (k + 1) =
(ProjFinSeq x0) . (k + 1)
by A10, A11, FINSEQ_4:15
.=
|(x0,(Base_FinSeq (n2,(k + 1))))| * (Base_FinSeq (n2,(k + 1)))
by A4, A10, A11, Def12
;
A15:
k < k + 1
by XREAL_1:29;
then A16:
k < len (ProjFinSeq x0)
by A11, XXREAL_0:2;
then
r = ((accum (ProjFinSeq x0)) /. k) + ((ProjFinSeq x0) /. (k + 1))
by Def10, A13;
then A17:
r . i = (r2 . i) + (r3 . i)
by RVSUM_1:11;
A18:
now ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i )assume A19:
i <= k + 1
;
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . iper cases
( i < k + 1 or i = k + 1 )
by A19, XXREAL_0:1;
suppose A20:
i < k + 1
;
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . ithen A21:
i <= k
by NAT_1:13;
((ProjFinSeq x0) /. (k + 1)) . i =
|(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2)
by A14, RVSUM_1:44
.=
|(x0,(Base_FinSeq (n2,(k + 1))))| * 0
by A4, A8, A9, A20, MATRIXR2:76
;
hence
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i
by A7, A8, A9, A12, A13, A16, A17, A21;
verum end; suppose A22:
i = k + 1
;
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . ithen A23:
((accum (ProjFinSeq x0)) /. k) . i = 0
by A7, A8, A9, A13, A15, A16;
((ProjFinSeq x0) /. (k + 1)) . i =
|(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2)
by A14, RVSUM_1:44
.=
|(x0,(Base_FinSeq (n2,(k + 1))))| * 1
by A4, A8, A9, A22, MATRIXR2:75
.=
x0 . (k + 1)
by A4, A10, A11, Th29
;
hence
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i
by A2, A8, A9, A17, A22, A23, FINSEQ_4:15;
verum end; end; end; now ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 )assume A24:
i > k + 1
;
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 then A25:
i > k
by A15, XXREAL_0:2;
((ProjFinSeq x0) /. (k + 1)) . i =
|(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2)
by A14, RVSUM_1:44
.=
|(x0,(Base_FinSeq (n2,(k + 1))))| * 0
by A4, A8, A9, A24, MATRIXR2:76
.=
0
;
hence
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
by A7, A8, A9, A12, A13, A16, A17, A25;
verum end; hence
( (
i <= k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & (
i > k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
by A18;
verum end; case
k < 1
;
( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )then A26:
k + 1
<= 0 + 1
by NAT_1:13;
then A27:
k = 0
by XREAL_1:6;
A28:
now ( i > 0 + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 )assume A29:
i > 0 + 1
;
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
(accum (ProjFinSeq x0)) /. 1
= (ProjFinSeq x0) . 1
by A5, A2, A3, FINSEQ_4:15;
then ((accum (ProjFinSeq x0)) /. 1) . i =
(|(x0,(Base_FinSeq (n2,1)))| * (Base_FinSeq (n2,1))) . i
by A5, A4, Def12
.=
|(x0,(Base_FinSeq (n2,1)))| * ((Base_FinSeq (n2,1)) . i2)
by RVSUM_1:44
.=
|(x0,(Base_FinSeq (n2,1)))| * 0
by A4, A9, A29, MATRIXR2:76
.=
0
;
hence
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
by A27;
verum end; A30:
now ( i <= 0 + 1 implies ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i )assume
i <= 0 + 1
;
((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . ithen A31:
i = 1
by A8, XXREAL_0:1;
(accum (ProjFinSeq x0)) /. 1
= (ProjFinSeq x0) . 1
by A5, A2, A3, FINSEQ_4:15;
then ((accum (ProjFinSeq x0)) /. 1) . 1 =
(|(x0,(Base_FinSeq (n2,1)))| * (Base_FinSeq (n2,1))) . 1
by A5, A4, Def12
.=
|(x0,(Base_FinSeq (n2,1)))| * ((Base_FinSeq (n2,1)) . 1)
by RVSUM_1:44
.=
|(x0,(Base_FinSeq (n2,1)))| * 1
by A5, A4, MATRIXR2:75
.=
x0 . 1
by A5, A4, Th29
;
hence
((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i
by A31;
verum end;
k <= 0
by A26, XREAL_1:6;
hence
( (
i <= k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & (
i > k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
by A30, A28;
verum end; end; end;
hence
( (
i <= k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & (
i > k + 1 implies
((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
;
verum
end;
hence
S1[
k + 1]
;
verum
end; reconsider r4 =
(accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0)) as
Element of
REAL n ;
A32:
len x0 = n
by CARD_1:def 7;
then A33:
len x0 = len r4
by CARD_1:def 7;
A34:
S1[
0 ]
;
A35:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A34, A6);
for
i being
Nat st 1
<= i &
i <= len r4 holds
((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i
then
x0 = (accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))
by A33, FINSEQ_1:14;
hence
x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0))
by A5, A2, FINSEQ_4:15;
verum end; end; end;
hence
x0 = Sum (ProjFinSeq x0)
by Def11; verum