defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]

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 S_{1}[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

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: S

proof

A3:
for n being Nat st S
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;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

S

proof

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
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[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 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

then 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;

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;

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;assume A4: S

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 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

A15:
len (f | n) = n
by A5, FINSEQ_3:53;
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;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

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

m9 < n9

f | n is one-to-one
by A7, FUNCT_1:52;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;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

then 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;

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;

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

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 S

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