let T be non empty TopStruct ; for f1, f2 being FinSequence of Curves T holds (Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)
defpred S1[ Nat] means for f1, f2 being FinSequence of Curves T st len f1 = $1 holds
(Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1);
A1:
S1[ 0 ]
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
let f1,
f2 be
FinSequence of
Curves T;
( len f1 = k + 1 implies (Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1) )
assume A7:
len f1 = k + 1
;
(Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)
then consider f3 being
FinSequence of
Curves T,
c being
Element of
Curves T such that A8:
f1 = f3 ^ <*c*>
by FINSEQ_2:19;
set f4 =
<*c*> ^ f2;
A9:
f1 ^ f2 = f3 ^ (<*c*> ^ f2)
by A8, FINSEQ_1:32;
A10:
len f1 = (len f3) + 1
by A8, FINSEQ_2:16;
per cases
( 1 > k or 1 <= k )
;
suppose A11:
1
> k
;
(Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)then A12:
len f3 = 0
by A10, A7, NAT_1:14;
f3 = {}
by A11, A10, A7, FINSEQ_1:20;
then A13:
f1 = <*c*>
by A8, FINSEQ_1:34;
thus (Partial_Sums (f1 ^ f2)) . (len f1) =
(f1 ^ f2) . 1
by A12, A10, Def13
.=
c
by A13, FINSEQ_1:41
.=
f1 . 1
by A13
.=
(Partial_Sums f1) . (len f1)
by A12, A10, Def13
;
verum end; suppose A14:
1
<= k
;
(Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)A15:
k < len f1
by A7, NAT_1:16;
len (f3 ^ (<*c*> ^ f2)) = k + (len (<*c*> ^ f2))
by A10, A7, FINSEQ_1:22;
then A16:
k < len (f3 ^ (<*c*> ^ f2))
by NAT_1:16;
then
k in Seg (len (f3 ^ (<*c*> ^ f2)))
by A14, FINSEQ_1:1;
then
k in Seg (len (Partial_Sums (f3 ^ (<*c*> ^ f2))))
by Def13;
then A17:
k in dom (Partial_Sums (f3 ^ (<*c*> ^ f2)))
by FINSEQ_1:def 3;
k in Seg (len f3)
by A14, A10, A7, FINSEQ_1:1;
then
k in Seg (len (Partial_Sums f3))
by Def13;
then A18:
k in dom (Partial_Sums f3)
by FINSEQ_1:def 3;
k in Seg (len f1)
by A14, A15, FINSEQ_1:1;
then
k in Seg (len (Partial_Sums f1))
by Def13;
then A19:
k in dom (Partial_Sums f1)
by FINSEQ_1:def 3;
A20:
(Partial_Sums (f3 ^ (<*c*> ^ f2))) /. k =
(Partial_Sums (f3 ^ (<*c*> ^ f2))) . k
by A17, PARTFUN1:def 6
.=
(Partial_Sums f3) . k
by A10, A7, A6
.=
(Partial_Sums f3) /. k
by A18, PARTFUN1:def 6
;
A21:
(Partial_Sums f1) /. k =
(Partial_Sums f1) . k
by A19, PARTFUN1:def 6
.=
(Partial_Sums f3) . k
by A8, A10, A7, A6
.=
(Partial_Sums f3) /. k
by A18, PARTFUN1:def 6
;
1
+ 1
<= k + 1
by A14, XREAL_1:6;
then A22:
1
<= k + 1
by XXREAL_0:2;
0 + (len f1) <= (len f1) + (len f2)
by XREAL_1:6;
then
k + 1
<= len (f1 ^ f2)
by A7, FINSEQ_1:22;
then
k + 1
in Seg (len (f1 ^ f2))
by A22, FINSEQ_1:1;
then A23:
k + 1
in dom (f1 ^ f2)
by FINSEQ_1:def 3;
k + 1
in Seg (len f1)
by A7, A22, FINSEQ_1:1;
then A24:
k + 1
in dom f1
by FINSEQ_1:def 3;
A25:
(f1 ^ f2) /. (k + 1) =
(f1 ^ f2) . (k + 1)
by A23, PARTFUN1:def 6
.=
f1 . (k + 1)
by A24, FINSEQ_1:def 7
.=
f1 /. (k + 1)
by A24, PARTFUN1:def 6
;
thus (Partial_Sums (f1 ^ f2)) . (len f1) =
((Partial_Sums f1) /. k) + (f1 /. (k + 1))
by A7, A9, A20, A21, A25, A14, A16, Def13
.=
(Partial_Sums f1) . (len f1)
by A14, A7, A15, Def13
;
verum end;
end;
A26:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A5);
let f1, f2 be FinSequence of Curves T; (Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)
thus
(Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)
by A26; verum