defpred S₁[ Element of NAT ] means for Fn being XFinSequence of
for Fi being XFinSequence of st Fi = Fn & dom Fn = $1 holds
Sum Fi = Sum Fn;
let Fn be XFinSequence of ; :: thesis: for Fi being XFinSequence of st Fi = Fn holds
Sum Fi = Sum Fn
let Fi be XFinSequence of ; :: thesis: ( Fi = Fn implies Sum Fi = Sum Fn )
assume A1: Fi = Fn ; :: thesis: Sum Fi = Sum Fn
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]
let Fn be XFinSequence of ; :: thesis: for Fi being XFinSequence of st Fi = Fn & dom Fn = k + 1 holds
Sum Fi = Sum Fn
let Fi be XFinSequence of ; :: thesis: ( Fi = Fn & dom Fn = k + 1 implies Sum Fi = Sum Fn )
assume that
A4: Fi = Fn and
A5: dom Fn = k + 1 ; :: thesis: Sum Fi = Sum Fn
A6: Fn | (k + 1) = Fn by A5, RELAT_1:98;
( k < k + 1 & len Fn = k + 1 ) by A5, NAT_1:13;
then len (Fn | k) = k by AFINSQ_1:14;
then A7: Sum (Fn | k) = Sum (Fi | k) by A3, A4;
A8: ( addint . (addint "**" (Fi | k)),(Fi . k) = (addint "**" (Fi | k)) + (Fi . k) & addnat . (addnat "**" (Fn | k)),(Fn . k) = (addnat "**" (Fn | k)) + (Fn . k) ) by BINOP_2:def 20, BINOP_2:def 23;
k < k + 1 by NAT_1:13;
then A9: k in dom Fn by A5, NAT_1:45;
then A10: addnat . (addnat "**" (Fn | k)),(Fn . k) = addnat "**" (Fn | (k + 1)) by Th42;
A11: Sum (Fn | k) = addnat "**" (Fn | k) by STIRL2_1:def 4;
addint . (addint "**" (Fi | k)),(Fi . k) = addint "**" (Fi | (k + 1)) by A4, A9, Th42;
hence Sum Fi = Sum Fn by A4, A8, A10, A7, A6, A11, STIRL2_1:def 4; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

let Fn be XFinSequence of ; :: thesis: for Fi being XFinSequence of st Fi = Fn & dom Fn = 0 holds
Sum Fi = Sum Fn
let Fi be XFinSequence of ; :: thesis: ( Fi = Fn & dom Fn = 0 implies Sum Fi = Sum Fn )
assume that
A13: Fi = Fn and
A14: dom Fn = 0 ; :: thesis: Sum Fi = Sum Fn
A15: len Fn = 0 by A14;
then A16: addnat "**" Fn = 0 by BINOP_2:5, STIRL2_1:def 3;
addint "**" Fi = 0 by A13, A15, BINOP_2:4, STIRL2_1:def 3;
hence Sum Fi = Sum Fn by A16, STIRL2_1:def 4; :: thesis: verum

end;

A17: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A12, A2);
dom Fn = len Fn ;
hence Sum Fi = Sum Fn by A17, A1; :: thesis: verum