defpred S₁[ Nat] means for f being natural-valued FinSequence
for n being Nat st len f = $1 & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f;
A1: S₁[ 0 ]

proof

let f be natural-valued FinSequence; :: thesis: for n being Nat st len f = 0 & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f
let n be Nat; :: thesis: ( len f = 0 & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) implies Sgm (rng f) = f )
assume that
A2: len f = 0 and
rng f c= Seg n and
for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ; :: thesis: Sgm (rng f) = f
f = {} by A2;
hence Sgm (rng f) = f by FINSEQ_3:43; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let f be natural-valued FinSequence; :: thesis: for n being Nat st len f = n + 1 & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f
let k be Nat; :: thesis: ( len f = n + 1 & rng f c= Seg k & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) implies Sgm (rng f) = f )
assume that
A5: len f = n + 1 and
A6: rng f c= Seg k and
A8: for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ; :: thesis: Sgm (rng f) = f
set fn = f | n;
A9: f = (f | n) ^ <*(f . (n + 1))*> by A5, FINSEQ_3:55;
then A10: rng (f | n) c= rng f by FINSEQ_1:29;
A11: dom (f | n) c= dom f by A9, FINSEQ_1:26;
A12: for i, j being Nat st i in dom (f | n) & j in dom (f | n) & i < j holds
(f | n) . i < (f | n) . j

proof

let i, j be Nat; :: thesis: ( i in dom (f | n) & j in dom (f | n) & i < j implies (f | n) . i < (f | n) . j )
assume that
A13: ( i in dom (f | n) & j in dom (f | n) ) and
A14: i < j ; :: thesis: (f | n) . i < (f | n) . j
( (f | n) . i = f . i & (f | n) . j = f . j ) by A9, A13, FINSEQ_1:def 7;
hence (f | n) . i < (f | n) . j by A8, A11, A13, A14; :: thesis: verum

end;

A15: len (f | n) = n by A5, FINSEQ_3:53;

A16: now :: thesis: for m9, n9 being Nat st m9 in rng (f | n) & n9 in {(f . (n + 1))} holds
m9 < n9

A17: ( n + 1 in Seg (n + 1) & dom f = Seg (n + 1) ) by A5, FINSEQ_1:4, FINSEQ_1:def 3;
let m9, n9 be Nat; :: thesis: ( m9 in rng (f | n) & n9 in {(f . (n + 1))} implies m9 < n9 )
assume that
A18: m9 in rng (f | n) and
A19: n9 in {(f . (n + 1))} ; :: thesis: m9 < n9
consider x being object such that
A20: x in dom (f | n) and
A21: (f | n) . x = m9 by A18, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A20;
A22: f . x = (f | n) . x by A9, A20, FINSEQ_1:def 7;
dom (f | n) = Seg n by A15, FINSEQ_1:def 3;
then x <= n by A20, FINSEQ_1:1;
then x < n + 1 by NAT_1:13;
then f . x < f . (n + 1) by A8, A11, A20, A17;
hence m9 < n9 by A19, A21, A22, TARSKI:def 1; :: thesis: verum

end;

A23: Sgm (rng (f | n)) = f | n by A4, A6, A15, A10, A12, XBOOLE_1:1;
A24: rng <*(f . (n + 1))*> = {(f . (n + 1))} by FINSEQ_1:39;
rng <*(f . (n + 1))*> c= rng f by A9, FINSEQ_1:30;
then A25: {(f . (n + 1))} c= Seg k by A6, A24;
then a25: {(f . (n + 1))} is included_in_Seg ;
A26: rng f = (rng (f | n)) \/ (rng <*(f . (n + 1))*>) by A9, FINSEQ_1:31;
A27: f . (n + 1) in {(f . (n + 1))} by TARSKI:def 1;
rng (f | n) c= Seg k by A6, A10;
then rng (f | n) is included_in_Seg ;
hence Sgm (rng f) = (f | n) ^ (Sgm {(f . (n + 1))}) by A26, A24, a25, A23, A16, FINSEQ_3:42
.= f by A9, A25, A27, FINSEQ_3:44 ;
:: thesis: verum

end;

let f be natural-valued FinSequence; :: thesis: ( rng f is included_in_Seg & f is increasing implies Sgm (rng f) = f )
assume A28: rng f is included_in_Seg ; :: thesis: ( not f is increasing or Sgm (rng f) = f )
assume f is increasing ; :: thesis: Sgm (rng f) = f
then xxx: for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j by SEQM_3:def 1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
then for g being natural-valued FinSequence
for n being Nat st len g = len f & rng g c= Seg n & ( for i, j being Nat st i in dom g & j in dom g & i < j holds
g . i < g . j ) holds
Sgm (rng g) = g ;
hence Sgm (rng f) = f by A28, xxx; :: thesis: verum