let A be RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( x in rng s2 iff x in C )
hereby :: thesis: ( x in C implies x in rng s2 )
assume x in rng s2 ; :: thesis: x in C
then consider i being object such that
A7: ( i in dom s2 & x = s2 . i ) by FUNCT_1:def 3;
( i in dom (Sgm (s " C)) & (Sgm (s " C)) . i in dom s ) by A7, FUNCT_1:11;
then (Sgm (s " C)) . i in rng (Sgm (s " C)) by FUNCT_1:3;
then (Sgm (s " C)) . i in s " C by A4, FINSEQ_1:def 13;
then ( (Sgm (s " C)) . i in dom s & s . ((Sgm (s " C)) . i) in C ) by FUNCT_1:def 7;
hence x in C by A7, FUNCT_1:12; :: thesis: verum
end;
assume A8: x in C ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
take s2 ; :: thesis: s2 is C -asc_ordering
s2 is weakly-ascending by A13;
hence s2 is C -asc_ordering by A6, A12; :: thesis: verum