defpred S₁[ Nat] means for F being FinSequence of F_Real
for G being FinSequence of INT.Ring st len F = $1 & F = G holds
Sum F = Sum G;
P1: S₁[ 0 ]

proof

let F be FinSequence of F_Real; :: thesis: for G being FinSequence of INT.Ring st len F = 0 & F = G holds
Sum F = Sum G
let G be FinSequence of INT.Ring; :: thesis: ( len F = 0 & F = G implies Sum F = Sum G )
assume AS1: ( len F = 0 & F = G ) ; :: thesis: Sum F = Sum G
then F = <*> the carrier of F_Real ;
then P1: Sum F = 0. F_Real by RLVECT_1:43
.= 0 ;
G = <*> REAL by AS1;
then G = <*> the carrier of INT.Ring ;
then Sum G = 0. INT.Ring by RLVECT_1:43;
hence Sum F = Sum G by P1; :: thesis: verum

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume AS1: S₁[n] ; :: thesis: S₁[n + 1]
let F be FinSequence of F_Real; :: thesis: for G being FinSequence of INT.Ring st len F = n + 1 & F = G holds
Sum F = Sum G
let G be FinSequence of INT.Ring; :: thesis: ( len F = n + 1 & F = G implies Sum F = Sum G )
assume AS2: ( len F = n + 1 & F = G ) ; :: thesis: Sum F = Sum G
reconsider F0 = F | n as FinSequence of F_Real ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom F by AS2, FINSEQ_1:def 3;
then F . (n + 1) in rng F by FUNCT_1:3;
then reconsider af = F . (n + 1) as Element of F_Real ;
P1: len F0 = n by FINSEQ_1:59, AS2, NAT_1:11;
then P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
F0 = F | (dom F0) by P4, FINSEQ_1:def 16;
then P3: Sum F = (Sum F0) + af by AS2, A9, RLVECT_1:38;
reconsider G0 = G | n as FinSequence of INT.Ring ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom G by AS2, FINSEQ_1:def 3;
then G . (n + 1) in rng G by FUNCT_1:3;
then reconsider bf = G . (n + 1) as Element of INT.Ring ;
( len G = n + 1 & G0 = G | (Seg n) ) by AS2, FINSEQ_1:def 16;
then G = G0 ^ <*bf*> by FINSEQ_3:55;
then Sum G = (Sum G0) + bf by FVSUM_1:71;
hence Sum F = Sum G by AS1, AS2, P1, P3; :: thesis: verum

end;

X1: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
let F be FinSequence of F_Real; :: thesis: for G being FinSequence of INT.Ring st F = G holds
Sum F = Sum G
let G be FinSequence of INT.Ring; :: thesis: ( F = G implies Sum F = Sum G )
assume X2: F = G ; :: thesis: Sum F = Sum G
len F is Nat ;
hence Sum F = Sum G by X1, X2; :: thesis: verum