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;
A1: 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 A2: ( Fi = Fn & dom Fn = 0 ) ; :: thesis: Sum Fi = Sum Fn
len Fn = 0 by A2;
then ( addnat "**" Fn = 0 & addint "**" Fi = 0 & addnat "**" Fn = Sum Fn ) by A2, BINOP_2:4, BINOP_2:5, STIRL2_1:def 3, STIRL2_1:def 4;
hence Sum Fi = Sum Fn ; :: thesis: verum

end;

A3: 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 A4: 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 A5: ( Fi = Fn & dom Fn = k + 1 ) ; :: thesis: Sum Fi = Sum Fn
A6: ( 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 23, GR_CY_1:14;
k < k + 1 by NAT_1:13;
then ( k in dom Fn & addnat is having_a_unity & addint is having_a_unity ) by A5, NAT_1:45;
then A7: ( addnat . (addnat "**" (Fn | k)),(Fn . k) = addnat "**" (Fn | (k + 1)) & addint . (addint "**" (Fi | k)),(Fi . k) = addint "**" (Fi | (k + 1)) ) by A5, Th42;
( k < k + 1 & len Fn = k + 1 ) by A5, NAT_1:13;
then ( len (Fn | k) = k & len (Fi | k) = k ) by A5, AFINSQ_1:14;
then ( Sum (Fn | k) = Sum (Fi | k) & Sum (Fi | k) = addint "**" (Fi | k) & Fn | (k + 1) = Fn & Fi | (k + 1) = Fi & Sum (Fn | k) = addnat "**" (Fn | k) ) by A4, A5, RELAT_1:98, STIRL2_1:def 4;
hence Sum Fi = Sum Fn by A5, A6, A7, STIRL2_1:def 4; :: thesis: verum

end;

A8: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A3);
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 A9: Fi = Fn ; :: thesis: Sum Fi = Sum Fn
dom Fn = len Fn ;
hence Sum Fi = Sum Fn by A8, A9; :: thesis: verum