let rF1, rF2 be real-valued XFinSequence; :: thesis:
set d = rF1;
set e = rF2;
assume that
A1: len rF1 = len rF2 and
A2: for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ; :: thesis:
reconsider d = rF1, e = rF2 as XFinSequence of REAL by Lm3;
A3: ( Sum d = addreal "**" d & Sum e = addreal "**" e ) by Th47;

per cases by NAT_1:14;

suppose A4: len d >= 1 ; :: thesis:

consider f being sequence of REAL such that
A5: f . 0 = d . 0 and
A6: for n being Nat st n + 1 < len d holds
f . (n + 1) = addreal . ((f . n),(d . (n + 1))) and
A7: Sum d = f . ((len d) - 1) by A4, Def8, A3;
consider g being sequence of REAL such that
A8: g . 0 = e . 0 and
A9: for n being Nat st n + 1 < len e holds
g . (n + 1) = addreal . ((g . n),(e . (n + 1))) and
A10: Sum e = g . ((len e) - 1) by A4, A1, Def8, A3;
defpred S₁[ Nat] means ( $1 in dom d implies f . $1 <= g . $1 );

A11: now :: thesis:

let i be Nat; :: thesis:
assume A12: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

proof

assume A13: i + 1 in dom d ; :: thesis:
then A14: i + 1 < len d by AFINSQ_1:86;
then A15: i < len d by NAT_1:13;
A16: d . (i + 1) <= e . (i + 1) by A2, A13;
A17: f . (i + 1) = addreal . ((f . i),(d . (i + 1))) by A6, A14
.= (f . i) + (d . (i + 1)) by BINOP_2:def 9 ;
g . (i + 1) = addreal . ((g . i),(e . (i + 1))) by A1, A9, A14
.= (g . i) + (e . (i + 1)) by BINOP_2:def 9 ;
hence f . (i + 1) <= g . (i + 1) by A12, A15, A17, A16, AFINSQ_1:86, XREAL_1:7; :: thesis:

end;

end;

reconsider ld = (len d) - 1 as Element of NAT by A4, NAT_1:21;
(len d) - 1 < (len d) - 0 by XREAL_1:10;
then A18: ld in len d by AFINSQ_1:86;
A19: S₁[ 0 ] by A2, A5, A8;
for i being Nat holds S₁[i] from NAT_1:sch 2(A19, A11);
hence Sum rF1 <= Sum rF2 by A1, A7, A10, A18; :: thesis:

end;

suppose len d = 0 ; :: thesis:

then ( Sum d = the_unity_wrt addreal & Sum e = the_unity_wrt addreal ) by Def8, A3, A1;
hence Sum rF1 <= Sum rF2 ; :: thesis:

end;

end;