let n be Nat; :: thesis: (Seg 1) --> n is increasing FinSequence of NAT
set f = (Seg 1) --> n;
B1: {n} c= NAT by ZFMISC_1:31, ORDINAL1:def 12;
a4: rng ((Seg 1) --> n) c= {n} by FUNCOP_1:13;
dom ((Seg 1) --> n) = Seg 1 by FUNCOP_1:13;
then (Seg 1) --> n is FinSequence by FINSEQ_1:def 2;
then reconsider f = (Seg 1) --> n as FinSequence of NAT by a4, FINSEQ_1:def 4, B1, XBOOLE_1:1;
for m, n being Nat st m in dom f & n in dom f & m < n holds
f . m < f . n

proof

let m, n be Nat; :: thesis: ( m in dom f & n in dom f & m < n implies f . m < f . n )
A0: dom f = {1} by FUNCOP_1:13, FINSEQ_1:2;
assume A1: ( m in dom f & n in dom f & m < n ) ; :: thesis: f . m < f . n
then ( m = 1 & n = 1 ) by A0, TARSKI:def 1;
hence f . m < f . n by A1; :: thesis: verum

end;

hence (Seg 1) --> n is increasing FinSequence of NAT by SEQM_3:def 1; :: thesis: verum