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 ;
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 ;
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 ;
then (Sgm (s " C)) . i in rng (Sgm (s " C)) by FUNCT_1:3;
then (Sgm (s " C)) . i in s " C by ;
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 ; :: 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 ;
k in s " C by ;
then k in rng (Sgm (s " C)) by ;
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 ;
then x = (s * (Sgm (s " C))) . i by ;
hence x in rng s2 by ; :: 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 ;
( i in dom (Sgm (s " C)) & j in dom (Sgm (s " C)) ) by ;
then A18: ( 1 <= i & j <= len (Sgm (s " C)) ) by ;
A19: ( (Sgm (s " C)) . i in dom s & (Sgm (s " C)) . j in dom s ) by ;
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 ;
A22: ( s . k = s /. k & s . l = s /. l ) by ;
( s2 . i = s2 /. i & s2 . j = s2 /. j ) by ;
then A23: ( s /. k = s2 /. i & s /. l = s2 /. j ) by ;
k < l by ;
then s /. k <= s /. l by ;
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 ; :: thesis: verum