let F be FinSequence; :: thesis: for m, n being Nat st m <= n holds
len (F | m) <= len (F | n)
let m, n be Nat; :: thesis: ( m <= n implies len (F | m) <= len (F | n) )
assume m <= n ; :: thesis: len (F | m) <= len (F | n)
then F | m = (F | n) | m by FINSEQ_1:82;
hence len (F | m) <= len (F | n) by FINSEQ_1:79; :: thesis: verum