let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
defpred S1[ Nat] means for F, G, H being FinSequence of the carrier of V st len F = $1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G);
now for k being Nat st ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ) holds
for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)let k be
Nat;
( ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ) implies for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) )assume A1:
for
F,
G,
H being
FinSequence of the
carrier of
V st
len F = k &
len F = len G &
len F = len H & ( for
k being
Nat st
k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
;
for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)let F,
G,
H be
FinSequence of the
carrier of
V;
( len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )assume that A2:
len F = k + 1
and A3:
len F = len G
and A4:
len F = len H
and A5:
for
k being
Nat st
k in dom F holds
H . k = (F /. k) + (G /. k)
;
Sum H = (Sum F) + (Sum G)reconsider f =
F | (Seg k),
g =
G | (Seg k),
h =
H | (Seg k) as
FinSequence of the
carrier of
V by FINSEQ_1:18;
A6:
len h = k
by A2, A4, FINSEQ_3:53;
A7:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A8:
k + 1
in dom G
by A2, A3, FINSEQ_1:def 3;
then A9:
G . (k + 1) in rng G
by FUNCT_1:def 3;
k + 1
in dom H
by A2, A4, A7, FINSEQ_1:def 3;
then A10:
H . (k + 1) in rng H
by FUNCT_1:def 3;
A11:
k + 1
in dom F
by A2, A7, FINSEQ_1:def 3;
then
F . (k + 1) in rng F
by FUNCT_1:def 3;
then reconsider v =
F . (k + 1),
u =
G . (k + 1),
w =
H . (k + 1) as
Element of
V by A9, A10;
A12:
w =
(F /. (k + 1)) + (G /. (k + 1))
by A5, A11
.=
v + (G /. (k + 1))
by A11, PARTFUN1:def 6
.=
v + u
by A8, PARTFUN1:def 6
;
G = g ^ <*u*>
by A2, A3, FINSEQ_3:55;
then A13:
Sum G = (Sum g) + (Sum <*u*>)
by RLVECT_1:41;
A14:
Sum <*v*> = v
by RLVECT_1:44;
A15:
len f = k
by A2, FINSEQ_3:53;
A16:
len g = k
by A2, A3, FINSEQ_3:53;
now for i being Nat st i in dom f holds
h . i = (f /. i) + (g /. i)let i be
Nat;
( i in dom f implies h . i = (f /. i) + (g /. i) )assume A17:
i in dom f
;
h . i = (f /. i) + (g /. i)then A18:
F . i = f . i
by FUNCT_1:47;
len f <= len F
by A2, A15, NAT_1:12;
then A19:
dom f c= dom F
by FINSEQ_3:30;
then
i in dom F
by A17;
then
i in dom G
by A3, FINSEQ_3:29;
then A20:
G /. i = G . i
by PARTFUN1:def 6;
i in dom h
by A15, A6, A17, FINSEQ_3:29;
then A21:
H . i = h . i
by FUNCT_1:47;
F /. i = F . i
by A17, A19, PARTFUN1:def 6;
then A22:
f /. i = F /. i
by A17, A18, PARTFUN1:def 6;
A23:
i in dom g
by A15, A16, A17, FINSEQ_3:29;
then
G . i = g . i
by FUNCT_1:47;
then
g /. i = G /. i
by A23, A20, PARTFUN1:def 6;
hence
h . i = (f /. i) + (g /. i)
by A5, A17, A21, A19, A22;
verum end; then A24:
Sum h = (Sum f) + (Sum g)
by A1, A15, A16, A6;
F = f ^ <*v*>
by A2, FINSEQ_3:55;
then A25:
Sum F = (Sum f) + (Sum <*v*>)
by RLVECT_1:41;
A26:
Sum <*u*> = u
by RLVECT_1:44;
H = h ^ <*w*>
by A2, A4, FINSEQ_3:55;
hence Sum H =
(Sum h) + (Sum <*w*>)
by RLVECT_1:41
.=
((Sum f) + (Sum g)) + (v + u)
by A24, A12, RLVECT_1:44
.=
(((Sum f) + (Sum g)) + v) + u
by RLVECT_1:def 3
.=
((Sum F) + (Sum g)) + u
by A25, A14, RLVECT_1:def 3
.=
(Sum F) + (Sum G)
by A13, A26, RLVECT_1:def 3
;
verum end;
then A27:
for k being Nat st S1[k] holds
S1[k + 1]
;
A28:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A28, A27);
hence
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
; verum