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

proof

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

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;

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;

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;

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;

suppose ex l being Nat st
( 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;

end;

end;

suppose ex k being Nat st
( 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

proof

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;

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;

suppose ex l being Nat st
( 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;

end;

end;

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

end;

end;

end;

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