let T be non empty TopStruct ; 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; ( 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
; ex P being Permutation of NAT st S2 * P is subsequence of S1
defpred S1[ object , object ] means S2 . $1 = S1 . $2;
A3:
for n being object st n in NAT holds
ex u being object st
( u in NAT & S1[n,u] )
consider f being Function such that
A6:
dom f = NAT
and
A7:
rng f c= NAT
and
A8:
for n being object st n in NAT holds
S1[n,f . n]
from FUNCT_1:sch 6(A3);
reconsider A = rng f as non empty Subset of NAT by A6, A7, RELAT_1:42;
defpred S2[ 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
object ;
FUNCT_1:def 4 ( 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
;
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:12;
hence
x1 = x2
by A2, A13;
verum
end;
A14:
for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } <> {}
A17:
for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT
A18:
for n being Nat
for x being set ex y being set st S2[n,x,y]
proof
let n be
Nat;
for x being set ex y being set st S2[n,x,y]let x be
set ;
ex y being set st S2[n,x,y]
end;
consider g being Function such that
A21:
dom g = NAT
and
A22:
g . 0 = min A
and
A23:
for n being Nat holds S2[n,g . n,g . (n + 1)]
from RECDEF_1:sch 1(A18);
defpred S3[ Nat] means g . $1 in NAT ;
A24:
for k being Nat st S3[k] holds
S3[k + 1]
A25:
S3[ 0 ]
by A22;
A26:
for k being Nat holds S3[k]
from NAT_1:sch 2(A25, A24);
for n being Nat holds g . n is real
then reconsider g1 = g as Real_Sequence by A21, SEQ_1:2;
A27:
g1 is increasing
A28:
rng g c= NAT
then reconsider g1 = g1 as increasing sequence of NAT by A21, A27, RELSET_1:4;
A31:
g1 is one-to-one
then A36:
rng (g ") = NAT
by A21, FUNCT_1:33;
A37:
rng f = rng g
then A50:
rng f = dom (g ")
by A31, FUNCT_1:33;
then
( dom ((g ") * f) = dom f & rng ((g ") * f) = rng (g ") )
by RELAT_1:27, RELAT_1:28;
then reconsider P = (g ") * f as sequence of NAT by A6, A36, FUNCT_2:def 1, RELSET_1:4;
rng (g ") = dom g
by A31, FUNCT_1:33;
then
rng P = NAT
by A21, A50, RELAT_1:28;
then
P is onto
by FUNCT_2:def 3;
then reconsider P = P as Permutation of NAT by A9, A31;
take
P "
; S2 * (P ") is subsequence of S1
( NAT = dom (S2 * (P ")) & NAT = dom (S1 * g) & ( for x being object st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x ) )
proof
thus
NAT = dom (S2 * (P "))
by FUNCT_2:def 1;
( NAT = dom (S1 * g) & ( for x being object st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x ) )
rng g c= dom S1
by A28, NORMSP_1:12;
hence
NAT = dom (S1 * g)
by A21, RELAT_1:27;
for x being object st x in NAT holds
(S2 * (P ")) . x = (S1 * g) . x
let x be
object ;
( x in NAT implies (S2 * (P ")) . x = (S1 * g) . x )
assume A51:
x in NAT
;
(S2 * (P ")) . x = (S1 * g) . x
then A52:
g . x in rng g
by A21, FUNCT_1:def 3;
then A53:
(f ") . (g . x) in dom f
by A9, A37, FUNCT_1:32;
dom (P ") = NAT
by FUNCT_2:def 1;
hence (S2 * (P ")) . x =
S2 . ((((g ") * f) ") . x)
by A51, FUNCT_1:13
.=
S2 . (((f ") * ((g ") ")) . x)
by A9, A31, FUNCT_1:44
.=
S2 . (((f ") * g) . x)
by A31, FUNCT_1:43
.=
S2 . ((f ") . (g . x))
by A21, A51, FUNCT_1:13
.=
S1 . (f . ((f ") . (g . x)))
by A6, A8, A53
.=
S1 . (g . x)
by A9, A37, A52, FUNCT_1:35
.=
(S1 * g) . x
by A21, A51, FUNCT_1:13
;
verum
end;
then
S2 * (P ") = S1 * g1
;
hence
S2 * (P ") is subsequence of S1
; verum