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;
A9: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom 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;
A14: x1 in dom S2 by A6, A10, NORMSP_1:17;
x2 in dom S2 by A6, A11, NORMSP_1:17;
hence x1 = x2 by A2, A13, A14, FUNCT_1:def 8; :: thesis: verum

end;

A15: 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 A16: { 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 A18: x in rng f ; :: thesis: x in m + 1
then reconsider x' = x as Element of NAT by A7;
x' < m + 1

proof

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

end;

then x' in { x'' where x'' is Element of NAT : x'' < 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;

A19: 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 consider k being Element of NAT such that
A20: k = z and
( k in rng f & k > m ) ;
thus z in NAT by A20; :: thesis: verum

end;

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;
A21: 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 x' = x as Element of NAT ;
set B = { k where k is Element of NAT : ( k in rng f & k > x' ) } ;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > x' ) } as Subset of NAT by A19;
reconsider B = B as non empty Subset of NAT by A15;
take min B ; :: thesis: S₂[n,x, min B]
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
min B = 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 min B = min B' )
assume that
A22: m = x and
A23: B' = { k where k is Element of NAT : ( k in rng f & k > m ) } ; :: thesis: min B = min B'
thus min B = min B' by A22, A23; :: thesis: verum

end;

suppose A24: 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
A25: 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 A24, A25; :: thesis: verum

end;

end;

end;

consider g being Function such that
A26: dom g = NAT and
A27: g . 0 = min A and
A28: for n being Element of NAT holds S₂[n,g . n,g . (n + 1)] from RECDEF_1:sch 1(A21);
defpred S₃[ Element of NAT ] means g . $1 in NAT ;
A29: S₃[ 0 ] by A27;
A30: 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 A19;
reconsider B = B as non empty Subset of NAT by A15;
g . (k + 1) = min B by A28;
hence S₃[k + 1] ; :: thesis: verum

end;

A31: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A29, A30);
A32: 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
A33: x in dom g and
A34: y = g . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A26, A33;
g . x in NAT by A31;
hence y in NAT by A34; :: thesis: verum

end;

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 A31;
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 A26, SEQ_1:4;
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 A31;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A15, A19;
g1 . (n + 1) = min B by A28;
then g1 . (n + 1) in B by XXREAL_2:def 7;
then consider k being Element of NAT such that
A35: k = g1 . (n + 1) and
k in rng f and
A36: k > m ;
thus not g1 . (n + 1) <= g1 . n by A35, A36; :: thesis: verum

end;

then reconsider g1 = g1 as increasing sequence of NAT by A32, A26, RELSET_1:11;
A37: g1 is one-to-one

proof

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

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

suppose n1 < n2 ; :: thesis: contradiction

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

end;

suppose n2 < n1 ; :: thesis: contradiction

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

end;

end;

end;

then A42: g " is one-to-one ;
A43: 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 A44: y in rng f ; :: thesis: y in rng g
then reconsider y' = y as Element of NAT by A7;
assume A45: not y in rng g ; :: thesis: contradiction
defpred S₄[ Element of NAT ] means g1 . $1 < y';
A46: S₄[ 0 ]

proof

assume A47: not g1 . 0 < y' ; :: thesis: contradiction
A48: min A <= y' by A44, XXREAL_2:def 7;
g . 0 in rng g by A26, FUNCT_1:def 5;
hence contradiction by A27, A45, A47, A48, XXREAL_0:1; :: thesis: verum

end;

A49: 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] )
assume A50: g1 . n < y' ; :: thesis: S₄[n + 1]
assume A51: not g1 . (n + 1) < y' ; :: thesis: contradiction
reconsider m = g . n as Element of NAT by A31;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A15, A19;
A52: g . (n + 1) = min B by A28;
y' in { k where k is Element of NAT : ( k in rng f & k > m ) } by A44, A50;
then A53: min B <= y' by XXREAL_2:def 7;
g . (n + 1) in rng g by A26, FUNCT_1:def 5;
hence contradiction by A45, A51, A52, A53, XXREAL_0:1; :: thesis: verum

end;

A55: for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A46, A49);
rng g c= y'

proof

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

end;

then rng g is finite by FINSET_1:13;
hence contradiction by A26, A37, 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
A58: x in dom g and
A59: y = g . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A26, A58;

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

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

hence y in rng f by A27, A59, 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;
A60: m + 1 = n ;
reconsider l = g . m as Element of NAT by A31;
reconsider B = { k where k is Element of NAT : ( k in rng f & k > l ) } as non empty Subset of NAT by A15, A19;
g . n = min B by A28, A60;
then y in B by A59, XXREAL_2:def 7;
then consider k being Element of NAT such that
A61: k = y and
A62: k in rng f and
k > l ;
thus y in rng f by A61, A62; :: thesis: verum

end;

end;

end;

then A63: rng f = dom (g " ) by A37, FUNCT_1:55;
then A64: ( dom ((g " ) * f) = dom f & rng ((g " ) * f) = rng (g " ) ) by RELAT_1:46, RELAT_1:47;
A65: rng (g " ) = dom g by A37, FUNCT_1:55;
rng (g " ) = NAT by A26, A37, FUNCT_1:55;
then reconsider P = (g " ) * f as Function of NAT ,NAT by A6, A64, FUNCT_2:def 1, RELSET_1:11;
P is bijective

proof

thus P is one-to-one by A9, A42; :: according to FUNCT_2:def 4 :: thesis: P is onto
thus rng P = NAT by A26, A63, A65, RELAT_1:47; :: according to FUNCT_2:def 3 :: thesis: verum

end;

then reconsider P = P as Permutation of NAT ;
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

A66: ( dom (P " ) = NAT & rng (P " ) c= NAT ) by FUNCT_2:def 1;
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 A32, NORMSP_1:17;
hence NAT = dom (S1 * g) by A26, 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 A67: x in NAT ; :: thesis: (S2 * (P " )) . x = (S1 * g) . x
then A68: g . x in rng g by A26, FUNCT_1:def 5;
then A69: (f " ) . (g . x) in dom f by A9, A43, FUNCT_1:54;
thus (S2 * (P " )) . x = S2 . ((((g " ) * f) " ) . x) by A66, A67, FUNCT_1:23
.= S2 . (((f " ) * ((g " ) " )) . x) by A9, A42, FUNCT_1:66
.= S2 . (((f " ) * g) . x) by A37, FUNCT_1:65
.= S2 . ((f " ) . (g . x)) by A26, A67, FUNCT_1:23
.= S1 . (f . ((f " ) . (g . x))) by A6, A8, A69
.= S1 . (g . x) by A9, A43, A68, FUNCT_1:57
.= (S1 * g) . x by A26, A67, FUNCT_1:23 ; :: thesis: verum

end;

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