let A be RelStr ; for B, C being Subset of A
for s being FinSequence of A st s is B -asc_ordering & C c= B holds
ex s2 being FinSequence of A st s2 is C -asc_ordering
let B, C be Subset of A; for s being FinSequence of A st s is B -asc_ordering & C c= B holds
ex s2 being FinSequence of A st s2 is C -asc_ordering
let s be FinSequence of A; ( s is B -asc_ordering & C c= B implies ex s2 being FinSequence of A st s2 is C -asc_ordering )
assume that
A1:
s is B -asc_ordering
and
A2:
C c= B
; ex s2 being FinSequence of A st s2 is C -asc_ordering
set s2 = s * (Sgm (s " C));
consider n being Nat such that
A3:
dom s = Seg n
by FINSEQ_1:def 2;
for x being object st x in s " C holds
x in Seg n
by A3, FUNCT_1:def 7;
then A4:
s " C c= Seg n
;
reconsider s2 = s * (Sgm (s " C)) as FinSequence by A3, A4;
A5:
rng s2 c= rng s
by RELAT_1:26;
rng s c= the carrier of A
by FINSEQ_1:def 4;
then
rng s2 c= the carrier of A
by A5;
then reconsider s2 = s2 as FinSequence of A by FINSEQ_1:def 4;
Sgm (s " C) is one-to-one
by A4, FINSEQ_3:92;
then A6:
s2 is one-to-one
by A1;
for x being object holds
( x in rng s2 iff x in C )
proof
let x be
object ;
( x in rng s2 iff x in C )
hereby ( x in C implies x in rng s2 )
end;
assume A8:
x in C
;
x in rng s2
then consider k being
object such that A9:
(
k in dom s &
x = s . k )
by A1, A2, FUNCT_1:def 3;
k in s " C
by A8, A9, FUNCT_1:def 7;
then
k in rng (Sgm (s " C))
by A4, FINSEQ_1:def 13;
then consider i being
object such that A10:
(
i in dom (Sgm (s " C)) &
k = (Sgm (s " C)) . i )
by FUNCT_1:def 3;
A11:
i in dom s2
by A9, A10, FUNCT_1:11;
then
x = (s * (Sgm (s " C))) . i
by A9, A10, FUNCT_1:12;
hence
x in rng s2
by A11, FUNCT_1:def 3;
verum
end;
then A12:
rng s2 = C
by TARSKI:2;
A13:
for n, m being Nat st n in dom s2 & m in dom s2 & n < m holds
s2 /. n <= s2 /. m
proof
let i,
j be
Nat;
( i in dom s2 & j in dom s2 & i < j implies s2 /. i <= s2 /. j )
assume that A14:
(
i in dom s2 &
j in dom s2 )
and A15:
i < j
;
s2 /. i <= s2 /. j
consider m being
Nat such that A16:
dom (Sgm (s " C)) = Seg m
by FINSEQ_1:def 2;
dom (Sgm (s " C)) = Seg (len (Sgm (s " C)))
by FINSEQ_1:def 3;
then A17:
len (Sgm (s " C)) = m
by A16, FINSEQ_1:6;
(
i in dom (Sgm (s " C)) &
j in dom (Sgm (s " C)) )
by A14, FUNCT_1:11;
then A18:
( 1
<= i &
j <= len (Sgm (s " C)) )
by A16, A17, FINSEQ_1:1;
A19:
(
(Sgm (s " C)) . i in dom s &
(Sgm (s " C)) . j in dom s )
by A14, FUNCT_1:11;
reconsider k =
(Sgm (s " C)) . i,
l =
(Sgm (s " C)) . j as
Nat ;
A20:
s is
weakly-ascending
by A1;
A21:
(
s . k = s2 . i &
s . l = s2 . j )
by A14, FUNCT_1:12;
A22:
(
s . k = s /. k &
s . l = s /. l )
by A19, PARTFUN1:def 6;
(
s2 . i = s2 /. i &
s2 . j = s2 /. j )
by A14, PARTFUN1:def 6;
then A23:
(
s /. k = s2 /. i &
s /. l = s2 /. j )
by A22, A21;
k < l
by A18, A15, A4, FINSEQ_1:def 13;
then
s /. k <= s /. l
by A19, A20;
hence
s2 /. i <= s2 /. j
by A23;
verum
end;
take
s2
; s2 is C -asc_ordering
s2 is weakly-ascending
by A13;
hence
s2 is C -asc_ordering
by A6, A12; verum