defpred S1[ 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: S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; :: thesis: S1[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 ;
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 ;
then reconsider ag = G . (n + 1) as Element of F_Rat ;
P1: len F0 = n by ;
len G0 = n by ;
then BP4: dom G0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by ;
BP3: Sum G = (Sum G0) + ag by ;
(Sum F0) + af = (Sum G0) + ag by AS1, AS2, P1;
hence Sum F = Sum G by ; :: thesis: verum
end;
X1: for n being Nat holds S1[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