let d, e be XFinSequence of NAT ; :: thesis: ( len d >= 1 & len d = len e & ( for i being Nat st i in dom d holds
d . i <= e . i ) implies Sum d <= Sum e )
assume that
A1: len d >= 1 and
A2: len d = len e and
A3: for i being Nat st i in dom d holds
d . i <= e . i ; :: thesis: Sum d <= Sum e
consider f being Function of NAT , NAT such that
A4: f . 0 = d . 0 and
A5: for n being Element of NAT st n + 1 < len d holds
f . (n + 1) = addnat . (f . n),(d . (n + 1)) and
A6: Sum d = f . ((len d) - 1) by A1, STIRL2_1:def 3;
consider g being Function of NAT , NAT such that
A7: g . 0 = e . 0 and
A8: for n being Element of NAT st n + 1 < len e holds
g . (n + 1) = addnat . (g . n),(e . (n + 1)) and
A9: Sum e = g . ((len e) - 1) by A1, A2, STIRL2_1:def 3;
defpred S₁[ Element of NAT ] means ( $1 in dom d implies f . $1 <= g . $1 );

A10: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A11: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A12: i + 1 in dom d ; :: thesis: f . (i + 1) <= g . (i + 1)
then A13: i + 1 < len d by NAT_1:45;
then A14: i < len d by NAT_1:13;
A15: d . (i + 1) <= e . (i + 1) by A3, A12;
A16: f . (i + 1) = addnat . (f . i),(d . (i + 1)) by A5, A13
.= (f . i) + (d . (i + 1)) by BINOP_2:def 23 ;
g . (i + 1) = addnat . (g . i),(e . (i + 1)) by A2, A8, A13
.= (g . i) + (e . (i + 1)) by BINOP_2:def 23 ;
hence f . (i + 1) <= g . (i + 1) by A11, A14, A16, A15, NAT_1:45, XREAL_1:9; :: thesis: verum

end;

end;

reconsider ld = (len d) - 1 as Element of NAT by A1, NAT_1:21;
(len d) - 1 < (len d) - 0 by XREAL_1:12;
then A17: ld in len d by NAT_1:45;
A18: S₁[ 0 ] by A3, A4, A7;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A18, A10);
hence Sum d <= Sum e by A2, A6, A9, A17; :: thesis: verum