let d, e be XFinSequence of ; :: 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 A1: ( len d >= 1 & len d = len e & ( 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
A2: ( f . 0 = d . 0 & ( for n being Element of NAT st n + 1 < len d holds
f . (n + 1) = addnat . (f . n),(d . (n + 1)) ) & Sum d = f . ((len d) - 1) ) by A1, STIRL2_1:def 3;
consider g being Function of NAT ,NAT such that
A3: ( g . 0 = e . 0 & ( for n being Element of NAT st n + 1 < len e holds
g . (n + 1) = addnat . (g . n),(e . (n + 1)) ) & Sum e = g . ((len e) - 1) ) by A1, STIRL2_1:def 3;
defpred S₁[ Element of NAT ] means ( $1 in dom d implies f . $1 <= g . $1 );
A4: S₁[ 0 ] by A1, A2, A3;

A5: now

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

proof

assume A7: i + 1 in dom d ; :: thesis: f . (i + 1) <= g . (i + 1)
then A8: i + 1 < len d by NAT_1:45;
then B9: i < len d by NAT_1:13;
A10: f . (i + 1) = addnat . (f . i),(d . (i + 1)) by A2, A8
.= (f . i) + (d . (i + 1)) by BINOP_2:def 23 ;
A11: g . (i + 1) = addnat . (g . i),(e . (i + 1)) by A1, A3, A8
.= (g . i) + (e . (i + 1)) by BINOP_2:def 23 ;
d . (i + 1) <= e . (i + 1) by A1, A7;
hence f . (i + 1) <= g . (i + 1) by A6, B9, A10, A11, NAT_1:45, XREAL_1:9; :: thesis: verum

end;

end;

A12: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A4, A5);
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 ld in len d by NAT_1:45;
hence Sum d <= Sum e by A1, A2, A3, A12; :: thesis: verum