let R be non empty transitive RelStr ; :: thesis: for f being sequence of R st f is weakly-ascending holds
for i, j being Nat st i < j holds
f . i <= f . j
let f be sequence of R; :: thesis: ( f is weakly-ascending implies for i, j being Nat st i < j holds
f . i <= f . j )
assume A1: f is weakly-ascending ; :: thesis: for i, j being Nat st i < j holds
f . i <= f . j
let i be Nat; :: thesis: for j being Nat st i < j holds
f . i <= f . j
defpred S₁[ Nat] means ( i < $1 implies f . i <= f . $1 );
A2: S₁[ 0 ] by NAT_1:2;
A3: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume that
A4: S₁[j] and
A5: i < j + 1 ; :: thesis: f . i <= f . (j + 1)
reconsider fj1 = f . (j + 1) as Element of R ;
A6: [(f . j),(f . (j + 1))] in the InternalRel of R by A1;
then A7: f . j <= fj1 ;
A8: i <= j by A5, NAT_1:13;

per cases ( i < j or i = j ) by A8, XXREAL_0:1;

suppose i < j ; :: thesis: f . i <= f . (j + 1)

hence f . i <= f . (j + 1) by A4, A7, ORDERS_2:3; :: thesis: verum

end;

suppose i = j ; :: thesis: f . i <= f . (j + 1)

hence f . i <= f . (j + 1) by A6; :: thesis: verum

end;

end;

end;

thus for j being Nat holds S₁[j] from NAT_1:sch 2(A2, A3); :: thesis: verum