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 )

A13: for n, m being Nat st n in dom s2 & m in dom s2 & n < m holds

s2 /. n <= s2 /. m

s2 is weakly-ascending by A13;

hence s2 is C -asc_ordering by A6, A12; :: thesis: verum

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

then A12:
rng s2 = C
by TARSKI:2;
let x be object ; :: thesis: ( x in rng s2 iff x in C )

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;hereby :: thesis: ( x in C implies x in rng s2 )

assume A8:
x in C
; :: thesis: x in rng s2assume
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;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

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

A13: for n, m being Nat st n in dom s2 & m in dom s2 & n < m holds

s2 /. n <= s2 /. m

proof

take
s2
; :: thesis: s2 is C -asc_ordering
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;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

s2 is weakly-ascending by A13;

hence s2 is C -asc_ordering by A6, A12; :: thesis: verum