defpred S1[ Nat] means for f being FinSequence of NAT
for n being Nat st len f = \$1 & rng f c= Seg n & f is one-to-one & ( 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: S1[ 0 ]
proof
let f be FinSequence of NAT ; :: thesis: for n being Nat st len f = 0 & rng f c= Seg n & f is one-to-one & ( 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 & f is one-to-one & ( 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
f is one-to-one 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
let f be FinSequence of NAT ; :: thesis: for n being Nat st len f = n + 1 & rng f c= Seg n & f is one-to-one & ( 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 & f is one-to-one & ( 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
A7: f is one-to-one 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 ;
then A10: rng (f | n) c= rng f by FINSEQ_1:29;
A11: dom (f | n) c= dom f by ;
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 ;
hence (f | n) . i < (f | n) . j by A8, A11, A13, A14; :: thesis: verum
end;
A15: len (f | n) = n by ;
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 ;
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 ;
reconsider x = x as Element of NAT by A20;
A22: f . x = (f | n) . x by ;
dom (f | n) = Seg n by ;
then x <= n by ;
then x < n + 1 by NAT_1:13;
then f . x < f . (n + 1) by A8, A11, A20, A17;
hence m9 < n9 by ; :: thesis: verum
end;
f | n is one-to-one by ;
then A23: Sgm (rng (f | n)) = f | n by ;
A24: rng <*(f . (n + 1))*> = {(f . (n + 1))} by FINSEQ_1:39;
rng <*(f . (n + 1))*> c= rng f by ;
then A25: {(f . (n + 1))} c= Seg k by ;
A26: rng f = (rng (f | n)) \/ (rng <*(f . (n + 1))*>) by ;
A27: f . (n + 1) in {(f . (n + 1))} by TARSKI:def 1;
rng (f | n) c= Seg k by ;
hence Sgm (rng f) = (f | n) ^ (Sgm {(f . (n + 1))}) by
.= f by ;
:: thesis: verum
end;
let f be FinSequence of NAT ; :: thesis: for n being Nat st f is one-to-one & 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: ( f is one-to-one & 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 A28: ( f is one-to-one & 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 ) ) ; :: thesis: Sgm (rng f) = f
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A3);
then for g being FinSequence of NAT
for n being Nat st len g = len f & rng g c= Seg n & g is one-to-one & ( 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; :: thesis: verum