defpred S₁[ Element of NAT ] means for F, Fi being XFinSequence of INT
for i being Integer st dom F = $1 & dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) holds
i * (Sum F) = Sum Fi;
let F, Fi be XFinSequence of INT ; :: thesis: for i being Integer st dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) holds
i * (Sum F) = Sum Fi
let i be Integer; :: thesis: ( dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) implies i * (Sum F) = Sum Fi )
assume A1: ( dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) ) ; :: thesis: i * (Sum F) = Sum Fi
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: k < k + 1 by NAT_1:13;
let F, Fi be XFinSequence of INT ; :: thesis: for i being Integer st dom F = k + 1 & dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) holds
i * (Sum F) = Sum Fi
let i be Integer; :: thesis: ( dom F = k + 1 & dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) implies i * (Sum F) = Sum Fi )
assume that
A5: dom F = k + 1 and
A6: dom F = dom Fi and
A7: for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ; :: thesis: i * (Sum F) = Sum Fi
A8: F | (k + 1) = F by A5, RELAT_1:98;
len F = k + 1 by A5;
then A9: len (F | k) = k by A4, AFINSQ_1:14;
k < k + 1 by NAT_1:13;
then A10: k in dom F by A5, NAT_1:45;
then addint . (addint "**" (F | k)),(F . k) = addint "**" (F | (k + 1)) by Th42;
then A11: Sum F = (Sum (F | k)) + (F . k) by A8, BINOP_2:def 20;
len Fi = k + 1 by A5, A6;
then A12: len (Fi | k) = k by A4, AFINSQ_1:14;
for n being Element of NAT st n in dom (F | k) holds
i * ((F | k) . n) = (Fi | k) . n

proof

let n be Element of NAT ; :: thesis: ( n in dom (F | k) implies i * ((F | k) . n) = (Fi | k) . n )
assume A13: n in dom (F | k) ; :: thesis: i * ((F | k) . n) = (Fi | k) . n
A14: ( n in dom F & (F | k) . n = F . n ) by A13, FUNCT_1:70, RELAT_1:86;
(Fi | k) . n = Fi . n by A9, A12, A13, FUNCT_1:70;
hence i * ((F | k) . n) = (Fi | k) . n by A7, A14; :: thesis: verum

end;

then A15: i * (Sum (F | k)) = Sum (Fi | k) by A3, A9, A12;
k < k + 1 by NAT_1:13;
then k in dom F by A5, NAT_1:45;
then A16: i * (F . k) = Fi . k by A7;
A17: Fi | (k + 1) = Fi by A5, A6, RELAT_1:98;
addint . (addint "**" (Fi | k)),(Fi . k) = addint "**" (Fi | (k + 1)) by A6, A10, Th42;
then Sum Fi = (Sum (Fi | k)) + (Fi . k) by A17, BINOP_2:def 20;
hence i * (Sum F) = Sum Fi by A11, A16, A15; :: thesis: verum

end;

A18: S₁[ 0 ]

proof

let F, Fi be XFinSequence of INT ; :: thesis: for i being Integer st dom F = 0 & dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) holds
i * (Sum F) = Sum Fi
let i be Integer; :: thesis: ( dom F = 0 & dom F = dom Fi & ( for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ) implies i * (Sum F) = Sum Fi )
assume that
A19: dom F = 0 and
A20: dom F = dom Fi and
for n being Element of NAT st n in dom F holds
i * (F . n) = Fi . n ; :: thesis: i * (Sum F) = Sum Fi
len F = 0 by A19;
then A21: addint "**" F = 0 by BINOP_2:4, STIRL2_1:def 3;
len Fi = 0 by A19, A20;
hence i * (Sum F) = Sum Fi by A21, BINOP_2:4, STIRL2_1:def 3; :: thesis: verum

end;

A22: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A2);
dom F = len F ;
hence i * (Sum F) = Sum Fi by A22, A1; :: thesis: verum