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 ]
P2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume AS1:
S1[
n]
;
S1[n + 1]
let F be
FinSequence of
F_Real;
for G being FinSequence of F_Rat st len F = n + 1 & F = G holds
Sum F = Sum Glet G be
FinSequence of
F_Rat;
( len F = n + 1 & F = G implies Sum F = Sum G )
assume AS2:
(
len F = n + 1 &
F = G )
;
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;
verum
end;
X1:
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
let F be FinSequence of F_Real; for G being FinSequence of F_Rat st F = G holds
Sum F = Sum G
let G be FinSequence of F_Rat; ( F = G implies Sum F = Sum G )
assume
F = G
; Sum F = Sum G
hence
Sum F = Sum G
by X1; verum