let T be non empty TopStruct ; :: thesis: for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds
ex P being Permutation of NAT st S2 * P is subsequence of S1
let S1, S2 be sequence of T; :: thesis: ( rng S2 c= rng S1 & S2 is one-to-one implies ex P being Permutation of NAT st S2 * P is subsequence of S1 )
assume that
A1: rng S2 c= rng S1 and
A2: S2 is one-to-one ; :: thesis: ex P being Permutation of NAT st S2 * P is subsequence of S1
defpred S₁[ set , set ] means S2 . $1 = S1 . $2;
A3: for n being set st n in NAT holds
ex u being set st
( u in NAT & S₁[n,u] )

proof

let n be set ; :: thesis: ( n in NAT implies ex u being set st
( u in NAT & S₁[n,u] ) )
assume n in NAT ; :: thesis: ex u being set st
( u in NAT & S₁[n,u] )
then n in dom S2 by NORMSP_1:17;
then S2 . n in rng S2 by FUNCT_1:def 5;
then consider m being set such that
A4: m in dom S1 and
A5: S2 . n = S1 . m by A1, FUNCT_1:def 5;
take m ; :: thesis: ( m in NAT & S₁[n,m] )
thus m in NAT by A4; :: thesis: S₁[n,m]
thus S₁[n,m] by A5; :: thesis: verum

end;

consider f being Function such that
A6: dom f = NAT and
A7: rng f c= NAT and
A8: for n being set st n in NAT holds
S₁[n,f . n] from WELLORD2:sch 1(A3);
reconsider A = rng f as non empty Subset of NAT by A6, A7, RELAT_1:65;
defpred S₂[ Element of NAT , set , set ] means for B being non empty Subset of NAT
for m being Element of NAT st m = $2 & B = { k where k is Element of NAT : ( k in rng f & k > m ) } holds
$3 = min B;
A9: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f . x1 = f . x2 ; :: thesis: x1 = x2
S2 . x2 = S1 . (f . x2) by A6, A8, A11;
then A13: S2 . x1 = S2 . x2 by A6, A8, A10, A12;
( x1 in dom S2 & x2 in dom S2 ) by A6, A10, A11, NORMSP_1:17;
hence x1 = x2 by A2, A13, FUNCT_1:def 8; :: thesis: verum

end;

A14: for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } <> {}

proof

let m be Element of NAT ; :: thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } <> {}
assume A15: { k where k is Element of NAT : ( k in rng f & k > m ) } = {} ; :: thesis: contradiction
rng f c= m + 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in m + 1 )
assume A16: x in rng f ; :: thesis: x in m + 1
then reconsider x9 = x as Element of NAT by A7;
x9 < m + 1

proof

assume x9 >= m + 1 ; :: thesis: contradiction
then x9 > m by NAT_1:13;
then x9 in { k where k is Element of NAT : ( k in rng f & k > m ) } by A16;
hence contradiction by A15; :: thesis: verum

end;

then x9 in { x99 where x99 is Element of NAT : x99 < m + 1 } ;
hence x in m + 1 by AXIOMS:30; :: thesis: verum

end;

then rng f is finite by FINSET_1:13;
hence contradiction by A6, A9, CARD_1:97; :: thesis: verum

end;

A17: for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT

proof

let m be Element of NAT ; :: thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { k where k is Element of NAT : ( k in rng f & k > m ) } or z in NAT )
assume z in { k where k is Element of NAT : ( k in rng f & k > m ) } ; :: thesis: z in NAT
then ex k being Element of NAT st
( k = z & k in rng f & k > m ) ;
hence z in NAT ; :: thesis: verum

end;

A18: for n being Element of NAT
for x being set ex y being set st S₂[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being set ex y being set st S₂[n,x,y]
let x be set ; :: thesis: ex y being set st S₂[n,x,y]

per cases ( x in NAT or not x in NAT ) ;

suppose x in NAT ; :: thesis: ex y being set st S₂[n,x,y]

then reconsider x9 = x as Element of NAT ;
set B = { k where k is Element of NAT : ( k in rng f & k > x9 ) } ;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > x9 ) } as Subset of NAT by A17;
reconsider B = B as non empty Subset of NAT by A14;
take min B ; :: thesis: S₂[n,x, min B]
let B9 be non empty Subset of NAT ; :: thesis: for m being Element of NAT st m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } holds
min B = min B9
let m be Element of NAT ; :: thesis: ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } implies min B = min B9 )
assume ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } ) ; :: thesis: min B = min B9
hence min B = min B9 ; :: thesis: verum

end;

suppose A19: not x in NAT ; :: thesis: ex y being set st S₂[n,x,y]

take 0 ; :: thesis: S₂[n,x, 0 ]
let B be non empty Subset of NAT ; :: thesis: for m being Element of NAT st m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } holds
0 = min B
let m be Element of NAT ; :: thesis: ( m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } implies 0 = min B )
assume that
A20: m = x and
B = { k where k is Element of NAT : ( k in rng f & k > m ) } ; :: thesis: 0 = min B
thus 0 = min B by A19, A20; :: thesis: verum

end;

end;

end;

consider g being Function such that
A21: dom g = NAT and
A22: g . 0 = min A and
A23: for n being Element of NAT holds S₂[n,g . n,g . (n + 1)] from RECDEF_1:sch 1(A18);
defpred S₃[ Element of NAT ] means g . $1 in NAT ;
A24: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume g . k in NAT ; :: thesis: S₃[k + 1]
then reconsider m = g . k as Element of NAT ;
set B = { l where l is Element of NAT : ( l in rng f & l > m ) } ;
reconsider B = { l where l is Element of NAT : ( l in rng f & l > m ) } as Subset of NAT by A17;
reconsider B = B as non empty Subset of NAT by A14;
g . (k + 1) = min B by A23;
hence S₃[k + 1] ; :: thesis: verum

end;

A25: S₃[ 0 ] by A22;
A26: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A25, A24);
for n being Element of NAT holds g . n is real

proof

let n be Element of NAT ; :: thesis: g . n is real
g . n in NAT by A26;
then reconsider w = g . n as Element of REAL ;
w is real ;
hence g . n is real ; :: thesis: verum

end;

then reconsider g1 = g as Real_Sequence by A21, SEQ_1:4;
A27: g1 is increasing

proof

let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: not g1 . (n + 1) <= g1 . n
reconsider m = g . n as Element of NAT by A26;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A14, A17;
g1 . (n + 1) = min B by A23;
then g1 . (n + 1) in B by XXREAL_2:def 7;
then ex k being Element of NAT st
( k = g1 . (n + 1) & k in rng f & k > m ) ;
hence not g1 . (n + 1) <= g1 . n ; :: thesis: verum

end;

A28: rng g c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in NAT )
assume y in rng g ; :: thesis: y in NAT
then consider x being set such that
A29: x in dom g and
A30: y = g . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A21, A29;
g . x in NAT by A26;
hence y in NAT by A30; :: thesis: verum

end;

then reconsider g1 = g1 as increasing sequence of NAT by A21, A27, RELSET_1:11;
A31: g1 is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 g1 or not x2 in proj1 g1 or not g1 . x1 = g1 . x2 or x1 = x2 )
assume that
A32: x1 in dom g1 and
A33: x2 in dom g1 and
A34: g1 . x1 = g1 . x2 ; :: thesis: x1 = x2
reconsider n2 = x2 as Element of NAT by A33;
reconsider n1 = x1 as Element of NAT by A32;
assume A35: x1 <> x2 ; :: thesis: contradiction

per cases ( n1 < n2 or n2 < n1 ) by A35, XXREAL_0:1;

suppose n1 < n2 ; :: thesis: contradiction

hence contradiction by A34, SEQM_3:7; :: thesis: verum

end;

suppose n2 < n1 ; :: thesis: contradiction

hence contradiction by A34, SEQM_3:7; :: thesis: verum

end;

end;

end;

then A36: rng (g " ) = NAT by A21, FUNCT_1:55;
A37: rng f = rng g

proof

thus for y being set st y in rng f holds
y in rng g :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: rng g c= rng f

proof

let y be set ; :: thesis: ( y in rng f implies y in rng g )
assume A38: y in rng f ; :: thesis: y in rng g
then reconsider y9 = y as Element of NAT by A7;
defpred S₄[ Element of NAT ] means g1 . $1 < y9;
assume A39: not y in rng g ; :: thesis: contradiction
A40: for n being Element of NAT st S₄[n] holds
S₄[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₄[n] implies S₄[n + 1] )
reconsider m = g . n as Element of NAT by A26;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A14, A17;
A41: ( g . (n + 1) = min B & g . (n + 1) in rng g ) by A21, A23, FUNCT_1:def 5;
assume g1 . n < y9 ; :: thesis: S₄[n + 1]
then y9 in { k where k is Element of NAT : ( k in rng f & k > m ) } by A38;
then A42: min B <= y9 by XXREAL_2:def 7;
assume not g1 . (n + 1) < y9 ; :: thesis: contradiction
hence contradiction by A39, A42, A41, XXREAL_0:1; :: thesis: verum

end;

A43: S₄[ 0 ]

proof

assume A44: not g1 . 0 < y9 ; :: thesis: contradiction
( min A <= y9 & g . 0 in rng g ) by A21, A38, FUNCT_1:def 5, XXREAL_2:def 7;
hence contradiction by A22, A39, A44, XXREAL_0:1; :: thesis: verum

end;

A45: for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A43, A40);
rng g c= y9

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in y9 )
assume y in rng g ; :: thesis: y in y9
then consider x being set such that
A46: x in dom g and
A47: y = g . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A21, A46;
g1 . x < y9 by A45;
then g1 . x in { i where i is Element of NAT : i < y9 } ;
hence y in y9 by A47, AXIOMS:30; :: thesis: verum

end;

then rng g is finite by FINSET_1:13;
hence contradiction by A21, A31, CARD_1:97; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in rng f )
assume y in rng g ; :: thesis: y in rng f
then consider x being set such that
A48: x in dom g and
A49: y = g . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A21, A48;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: y in rng f

hence y in rng f by A22, A49, XXREAL_2:def 7; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: y in rng f

then n > 0 by NAT_1:3;
then n + 1 > 0 + 1 by XREAL_1:8;
then 1 <= n by NAT_1:13;
then reconsider m = n - 1 as Element of NAT by INT_1:18;
reconsider l = g . m as Element of NAT by A26;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > l ) } as non empty Subset of NAT by A14, A17;
m + 1 = n ;
then g . n = min B by A23;
then y in B by A49, XXREAL_2:def 7;
then ex k being Element of NAT st
( k = y & k in rng f & k > l ) ;
hence y in rng f ; :: thesis: verum

end;

end;

end;

then A50: rng f = dom (g " ) by A31, FUNCT_1:55;
then ( dom ((g " ) * f) = dom f & rng ((g " ) * f) = rng (g " ) ) by RELAT_1:46, RELAT_1:47;
then reconsider P = (g " ) * f as Function of NAT ,NAT by A6, A36, FUNCT_2:def 1, RELSET_1:11;
rng (g " ) = dom g by A31, FUNCT_1:55;
then rng P = NAT by A21, A50, RELAT_1:47;
then P is onto by FUNCT_2:def 3;
then reconsider P = P as Permutation of NAT by A9, A31;
take P " ; :: thesis: S2 * (P " ) is subsequence of S1
( NAT = dom (S2 * (P " )) & NAT = dom (S1 * g) & ( for x being set st x in NAT holds
(S2 * (P " )) . x = (S1 * g) . x ) )

proof

thus NAT = dom (S2 * (P " )) by FUNCT_2:def 1; :: thesis: ( NAT = dom (S1 * g) & ( for x being set st x in NAT holds
(S2 * (P " )) . x = (S1 * g) . x ) )
rng g c= dom S1 by A28, NORMSP_1:17;
hence NAT = dom (S1 * g) by A21, RELAT_1:46; :: thesis: for x being set st x in NAT holds
(S2 * (P " )) . x = (S1 * g) . x
let x be set ; :: thesis: ( x in NAT implies (S2 * (P " )) . x = (S1 * g) . x )
assume A51: x in NAT ; :: thesis: (S2 * (P " )) . x = (S1 * g) . x
then A52: g . x in rng g by A21, FUNCT_1:def 5;
then A53: (f " ) . (g . x) in dom f by A9, A37, FUNCT_1:54;
dom (P " ) = NAT by FUNCT_2:def 1;
hence (S2 * (P " )) . x = S2 . ((((g " ) * f) " ) . x) by A51, FUNCT_1:23
.= S2 . (((f " ) * ((g " ) " )) . x) by A9, A31, FUNCT_1:66
.= S2 . (((f " ) * g) . x) by A31, FUNCT_1:65
.= S2 . ((f " ) . (g . x)) by A21, A51, FUNCT_1:23
.= S1 . (f . ((f " ) . (g . x))) by A6, A8, A53
.= S1 . (g . x) by A9, A37, A52, FUNCT_1:57
.= (S1 * g) . x by A21, A51, FUNCT_1:23 ;
:: thesis: verum

end;

then S2 * (P " ) = S1 * g1 by FUNCT_1:9;
hence S2 * (P " ) is subsequence of S1 ; :: thesis: verum