let k be Nat; :: thesis: for t being 1 _greater Nat holds [.0,((k + 1) * (t ")).[ \/ [.((k + 1) * (t ")),((k + 2) * (t ")).[ = [.0,((k + 2) * (t ")).[
let t be 1 _greater Nat; :: thesis: [.0,((k + 1) * (t ")).[ \/ [.((k + 1) * (t ")),((k + 2) * (t ")).[ = [.0,((k + 2) * (t ")).[
( 0 <= (k + 1) * (t ") & (k + 1) * (t ") <= (k + 2) * (t ") )

proof

k + 1 <= (k + 1) + 1 by XREAL_1:31;
hence ( 0 <= (k + 1) * (t ") & (k + 1) * (t ") <= (k + 2) * (t ") ) by XREAL_1:64; :: thesis: verum

end;

hence [.0,((k + 1) * (t ")).[ \/ [.((k + 1) * (t ")),((k + 2) * (t ")).[ = [.0,((k + 2) * (t ")).[ by XXREAL_1:168; :: thesis: verum