let A be transitive RelStr ; :: thesis: for B, C being Subset of A

for s1 being FinSequence of A

for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let B, C be Subset of A; :: thesis: for s1 being FinSequence of A

for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let s1 be FinSequence of A; :: thesis: for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let x be Element of A; :: thesis: ( s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) implies ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering ) )

assume that

A1: s1 is C -asc_ordering and

A2: not x in C and

A3: B = C \/ {x} and

A4: for y being Element of A st y in C holds

y <= x ; :: thesis: ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

A5: s1 is weakly-ascending by A1;

set sx = <*x*>;

not B is empty by A3;

then reconsider sx = <*x*> as FinSequence of the carrier of A by FINSEQ_1:74;

reconsider sx = sx as FinSequence of A ;

set s2 = s1 ^ sx;

take s1 ^ sx ; :: thesis: ( s1 ^ sx = s1 ^ <*x*> & s1 ^ sx is B -asc_ordering )

A6: rng (s1 ^ sx) = (rng sx) \/ (rng s1) by FINSEQ_1:31

.= B by A3, A1, FINSEQ_1:38 ;

{x} misses C by A2, ZFMISC_1:50;

then rng sx misses rng s1 by A1, FINSEQ_1:38;

then A7: s1 ^ sx is one-to-one by A1, FINSEQ_3:91;

for n, m being Nat st n in dom (s1 ^ sx) & m in dom (s1 ^ sx) & n < m holds

(s1 ^ sx) /. n <= (s1 ^ sx) /. m

hence ( s1 ^ sx = s1 ^ <*x*> & s1 ^ sx is B -asc_ordering ) by A6, A7; :: thesis: verum

for s1 being FinSequence of A

for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let B, C be Subset of A; :: thesis: for s1 being FinSequence of A

for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let s1 be FinSequence of A; :: thesis: for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) holds

ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

let x be Element of A; :: thesis: ( s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds

y <= x ) implies ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering ) )

assume that

A1: s1 is C -asc_ordering and

A2: not x in C and

A3: B = C \/ {x} and

A4: for y being Element of A st y in C holds

y <= x ; :: thesis: ex s2 being FinSequence of A st

( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )

A5: s1 is weakly-ascending by A1;

set sx = <*x*>;

not B is empty by A3;

then reconsider sx = <*x*> as FinSequence of the carrier of A by FINSEQ_1:74;

reconsider sx = sx as FinSequence of A ;

set s2 = s1 ^ sx;

take s1 ^ sx ; :: thesis: ( s1 ^ sx = s1 ^ <*x*> & s1 ^ sx is B -asc_ordering )

A6: rng (s1 ^ sx) = (rng sx) \/ (rng s1) by FINSEQ_1:31

.= B by A3, A1, FINSEQ_1:38 ;

{x} misses C by A2, ZFMISC_1:50;

then rng sx misses rng s1 by A1, FINSEQ_1:38;

then A7: s1 ^ sx is one-to-one by A1, FINSEQ_3:91;

for n, m being Nat st n in dom (s1 ^ sx) & m in dom (s1 ^ sx) & n < m holds

(s1 ^ sx) /. n <= (s1 ^ sx) /. m

proof

then
s1 ^ sx is weakly-ascending
;
let n, m be Nat; :: thesis: ( n in dom (s1 ^ sx) & m in dom (s1 ^ sx) & n < m implies (s1 ^ sx) /. n <= (s1 ^ sx) /. m )

assume that

A8: n in dom (s1 ^ sx) and

A9: m in dom (s1 ^ sx) and

A10: n < m ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

end;assume that

A8: n in dom (s1 ^ sx) and

A9: m in dom (s1 ^ sx) and

A10: n < m ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

per cases
( m in dom s1 or ex k being Nat st

( k in dom sx & m = (len s1) + k ) ) by A9, FINSEQ_1:25;

end;

( k in dom sx & m = (len s1) + k ) ) by A9, FINSEQ_1:25;

suppose A11:
m in dom s1
; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

then
(s1 ^ sx) . m = s1 . m
by FINSEQ_1:def 7;

then (s1 ^ sx) /. m = s1 . m by A9, PARTFUN1:def 6;

then A12: (s1 ^ sx) /. m = s1 /. m by A11, PARTFUN1:def 6;

end;then (s1 ^ sx) /. m = s1 . m by A9, PARTFUN1:def 6;

then A12: (s1 ^ sx) /. m = s1 /. m by A11, PARTFUN1:def 6;

per cases
( n in dom s1 or ex l being Nat st

( l in dom sx & n = (len s1) + l ) ) by A8, FINSEQ_1:25;

end;

( l in dom sx & n = (len s1) + l ) ) by A8, FINSEQ_1:25;

suppose A13:
n in dom s1
; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

then
(s1 ^ sx) . n = s1 . n
by FINSEQ_1:def 7;

then (s1 ^ sx) /. n = s1 . n by A8, PARTFUN1:def 6;

then A14: (s1 ^ sx) /. n = s1 /. n by A13, PARTFUN1:def 6;

s1 /. n <= s1 /. m by A5, A11, A13, A10;

hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by A12, A14; :: thesis: verum

end;then (s1 ^ sx) /. n = s1 . n by A8, PARTFUN1:def 6;

then A14: (s1 ^ sx) /. n = s1 /. n by A13, PARTFUN1:def 6;

s1 /. n <= s1 /. m by A5, A11, A13, A10;

hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by A12, A14; :: thesis: verum

suppose
ex l being Nat st

( l in dom sx & n = (len s1) + l ) ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

( l in dom sx & n = (len s1) + l ) ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

then consider l being Nat such that

A15: ( l in dom sx & n = (len s1) + l ) ;

m in Seg (len s1) by A11, FINSEQ_1:def 3;

then A16: m <= len s1 by FINSEQ_1:1;

l in Seg 1 by A15, FINSEQ_1:def 8;

then l = 1 by FINSEQ_1:2, TARSKI:def 1;

then m < n by A15, A16, NAT_1:13;

hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by A10; :: thesis: verum

end;A15: ( l in dom sx & n = (len s1) + l ) ;

m in Seg (len s1) by A11, FINSEQ_1:def 3;

then A16: m <= len s1 by FINSEQ_1:1;

l in Seg 1 by A15, FINSEQ_1:def 8;

then l = 1 by FINSEQ_1:2, TARSKI:def 1;

then m < n by A15, A16, NAT_1:13;

hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by A10; :: thesis: verum

suppose
ex k being Nat st

( k in dom sx & m = (len s1) + k ) ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

( k in dom sx & m = (len s1) + k ) ; :: thesis: (s1 ^ sx) /. n <= (s1 ^ sx) /. m

then consider k being Nat such that

A17: ( k in dom sx & m = (len s1) + k ) ;

k in Seg (len sx) by A17, FINSEQ_1:def 3;

then k in Seg 1 by FINSEQ_1:40;

then A18: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then (s1 ^ sx) . m = x by A17, FINSEQ_1:42;

then A19: (s1 ^ sx) /. m = x by A9, PARTFUN1:def 6;

(s1 ^ sx) /. n in C

end;A17: ( k in dom sx & m = (len s1) + k ) ;

k in Seg (len sx) by A17, FINSEQ_1:def 3;

then k in Seg 1 by FINSEQ_1:40;

then A18: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then (s1 ^ sx) . m = x by A17, FINSEQ_1:42;

then A19: (s1 ^ sx) /. m = x by A9, PARTFUN1:def 6;

(s1 ^ sx) /. n in C

proof
end;

hence
(s1 ^ sx) /. n <= (s1 ^ sx) /. m
by A19, A4; :: thesis: verumper cases
( n in dom s1 or ex l being Nat st

( l in dom sx & n = (len s1) + l ) ) by A8, FINSEQ_1:25;

end;

( l in dom sx & n = (len s1) + l ) ) by A8, FINSEQ_1:25;

suppose A20:
n in dom s1
; :: thesis: (s1 ^ sx) /. n in C

then A21:
(s1 ^ sx) . n = s1 . n
by FINSEQ_1:def 7;

s1 . n in rng s1 by A20, FUNCT_1:3;

hence (s1 ^ sx) /. n in C by A21, A1, A8, PARTFUN1:def 6; :: thesis: verum

end;s1 . n in rng s1 by A20, FUNCT_1:3;

hence (s1 ^ sx) /. n in C by A21, A1, A8, PARTFUN1:def 6; :: thesis: verum

suppose
ex l being Nat st

( l in dom sx & n = (len s1) + l ) ; :: thesis: (s1 ^ sx) /. n in C

( l in dom sx & n = (len s1) + l ) ; :: thesis: (s1 ^ sx) /. n in C

then consider l being Nat such that

A22: ( l in dom sx & n = (len s1) + l ) ;

l in Seg (len sx) by A22, FINSEQ_1:def 3;

then l in Seg 1 by FINSEQ_1:40;

then m = n by A17, A22, A18, FINSEQ_1:2, TARSKI:def 1;

hence (s1 ^ sx) /. n in C by A10; :: thesis: verum

end;A22: ( l in dom sx & n = (len s1) + l ) ;

l in Seg (len sx) by A22, FINSEQ_1:def 3;

then l in Seg 1 by FINSEQ_1:40;

then m = n by A17, A22, A18, FINSEQ_1:2, TARSKI:def 1;

hence (s1 ^ sx) /. n in C by A10; :: thesis: verum

hence ( s1 ^ sx = s1 ^ <*x*> & s1 ^ sx is B -asc_ordering ) by A6, A7; :: thesis: verum