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 ;
{x} misses C by ;
then rng sx misses rng s1 by ;
then A7: s1 ^ sx is one-to-one by ;
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 ;
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 ;
then A12: (s1 ^ sx) /. m = s1 /. m by ;
per cases ( n in dom s1 or ex l being Nat st
( l in dom sx & n = (len s1) + l ) )
by ;
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 ;
then A14: (s1 ^ sx) /. n = s1 /. n by ;
s1 /. n <= s1 /. m by A5, A11, A13, A10;
hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by ; :: 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 ;
then A16: m <= len s1 by FINSEQ_1:1;
l in Seg 1 by ;
then l = 1 by ;
then m < n by ;
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 ;
then k in Seg 1 by FINSEQ_1:40;
then A18: k = 1 by ;
then (s1 ^ sx) . m = x by ;
then A19: (s1 ^ sx) /. m = x by ;
(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 ;
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 ;
hence (s1 ^ sx) /. n in C by ; :: 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 ;
then l in Seg 1 by FINSEQ_1:40;
then m = n by ;
hence (s1 ^ sx) /. n in C by A10; :: thesis: verum
end;
end;
end;
hence (s1 ^ sx) /. n <= (s1 ^ sx) /. m by ; :: 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