let F, G be FinSequence of F_Real; :: thesis: ( len F = len G & ( for i being Nat st i in dom F holds
F . i <= G . i ) implies Sum F <= Sum G )
assume A1: ( len F = len G & ( for i being Nat st i in dom F holds
F . i <= G . i ) ) ; :: thesis: Sum F <= Sum G
Sum F <= Sum G

proof

defpred S₁[ Nat] means for F1, G1 being FinSequence of F_Real st len F1 = $1 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) holds
Sum F1 <= Sum G1;
A2: S₁[ 0 ]

proof

let F1, G1 be FinSequence of F_Real; :: thesis: ( len F1 = 0 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) implies Sum F1 <= Sum G1 )
assume A3: ( len F1 = 0 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) ) ; :: thesis: Sum F1 <= Sum G1
Sum F1 <= Sum G1

proof

( F1 = <*> the carrier of F_Real & G1 = <*> the carrier of F_Real ) by A3;
hence Sum F1 <= Sum G1 ; :: thesis: verum

end;

hence Sum F1 <= Sum G1 ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
for F1, G1 being FinSequence of F_Real st len F1 = n + 1 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) holds
Sum F1 <= Sum G1

proof

let F1, G1 be FinSequence of F_Real; :: thesis: ( len F1 = n + 1 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) implies Sum F1 <= Sum G1 )
assume A7: ( len F1 = n + 1 & len F1 = len G1 & ( for i being Nat st i in dom F1 holds
F1 . i <= G1 . i ) ) ; :: thesis: Sum F1 <= Sum G1
Sum F1 <= Sum G1

proof

reconsider F0 = F1 | n as FinSequence of F_Real ;
reconsider G0 = G1 | n as FinSequence of F_Real ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A8: ( n + 1 in dom F1 & n + 1 in dom G1 ) by A7, FINSEQ_1:def 3;
A9: ( len F0 = n & len G0 = n ) by FINSEQ_1:59, A7, NAT_1:11;
then A10: ( dom F0 = Seg n & dom G0 = Seg n ) by FINSEQ_1:def 3;
( dom F1 = Seg (n + 1) & dom G1 = Seg (n + 1) ) by A7, FINSEQ_1:def 3;
then A11: ( dom F0 c= dom F1 & dom G0 c= dom G1 ) by A10, FINSEQ_1:5, NAT_1:11;
F1 . (n + 1) in rng F1 by A8, FUNCT_1:3;
then reconsider Fn1 = F1 . (n + 1) as Element of F_Real ;
G1 . (n + 1) in rng G1 by A8, FUNCT_1:3;
then reconsider Gn1 = G1 . (n + 1) as Element of F_Real ;
F1 = F0 ^ <*(F1 /. (len F1))*> by FINSEQ_5:21, A7
.= F0 ^ <*Fn1*> by A7, A8, PARTFUN1:def 6 ;
then A14: Sum F1 = (Sum F0) + Fn1 by FVSUM_1:71;
G1 = G0 ^ <*(G1 /. (len G1))*> by FINSEQ_5:21, A7
.= G0 ^ <*Gn1*> by A7, A8, PARTFUN1:def 6 ;
then A15: Sum G1 = (Sum G0) + Gn1 by FVSUM_1:71;
for i being Nat st i in dom F0 holds
F0 . i <= G0 . i

proof

let i be Nat; :: thesis: ( i in dom F0 implies F0 . i <= G0 . i )
assume A16: i in dom F0 ; :: thesis: F0 . i <= G0 . i
A17: F0 . i = (F1 | (dom F0)) . i by A9, FINSEQ_1:def 3
.= F1 . i by A16, FUNCT_1:49 ;
G0 . i = G1 . i by A10, A16, FUNCT_1:49;
hence F0 . i <= G0 . i by A11, A16, A17, A7; :: thesis: verum

end;

then A19: Sum F0 <= Sum G0 by A6, A9;
Fn1 <= Gn1 by A7, A8;
hence Sum F1 <= Sum G1 by A14, A15, A19, XREAL_1:7; :: thesis: verum

end;

hence Sum F1 <= Sum G1 ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A5);
hence Sum F <= Sum G by A1; :: thesis: verum

end;

hence Sum F <= Sum G ; :: thesis: verum