defpred S₁[ Nat] means for F being FinSequence of F_Real
for G being FinSequence of F_Rat 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 F_Rat st len F = 0 & F = G holds
Sum F = Sum G
let G be FinSequence of F_Rat; :: thesis: ( len F = 0 & F = G implies Sum F = Sum G )
assume AS1: ( len F = 0 & F = G ) ; :: thesis: Sum F = Sum G
F = <*> the carrier of F_Real by AS1;
then X1: Sum F = 0. F_Real by RLVECT_1:43
.= 0 ;
G = <*> the carrier of F_Rat by AS1;
then Sum G = 0. F_Rat by RLVECT_1:43
.= 0 ;
hence Sum F = Sum G by X1; :: 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 F_Rat st len F = n + 1 & F = G holds
Sum F = Sum G
let G be FinSequence of F_Rat; :: 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 ;
reconsider G0 = G | n as FinSequence of F_Rat ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A70: 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 ;
G . (n + 1) in rng G by AS2, A70, FUNCT_1:3;
then reconsider ag = G . (n + 1) as Element of F_Rat ;
P1: len F0 = n by FINSEQ_1:59, AS2, NAT_1:11;
len G0 = n by FINSEQ_1:59, AS2, NAT_1:11;
then BP4: dom G0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
BP3: Sum G = (Sum G0) + ag by AS2, A9, BP4, RLVECT_1:38;
(Sum F0) + af = (Sum G0) + ag by AS1, AS2, P1;
hence Sum F = Sum G by AS2, A9, BP3, BP4, RLVECT_1:38; :: 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 F_Rat st F = G holds
Sum F = Sum G
let G be FinSequence of F_Rat; :: thesis: ( F = G implies Sum F = Sum G )
assume F = G ; :: thesis: Sum F = Sum G
hence Sum F = Sum G by X1; :: thesis: verum