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 S1[ Nat] means ( i < $1 implies f . i <= f . $1 );
A2: S1[ 0 ] by NAT_1:2;
A3: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume that
A4: S1[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 S1[j] from NAT_1:sch 2(A2, A3); :: thesis: verum