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
x <= y ) holds
ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & 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
x <= y ) holds
ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & 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
x <= y ) holds
ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & 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
x <= y ) implies ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & 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
x <= y ; :: thesis: ex s2 being FinSequence of A st
( s2 = <*x*> ^ s1 & 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;
set s2 = sx ^ s1;
take sx ^ s1 ; :: thesis: ( sx ^ s1 = <*x*> ^ s1 & sx ^ s1 is B -asc_ordering )
thus sx ^ s1 = <*x*> ^ s1 ; :: thesis: sx ^ s1 is B -asc_ordering
A6: rng (sx ^ s1) = (rng sx) \/ (rng s1) by FINSEQ_1:31
.= B by ;
{x} misses C by ;
then rng sx misses rng s1 by ;
then A7: sx ^ s1 is one-to-one by ;
for n, m being Nat st n in dom (sx ^ s1) & m in dom (sx ^ s1) & n < m holds
(sx ^ s1) /. n <= (sx ^ s1) /. m
proof
let n, m be Nat; :: thesis: ( n in dom (sx ^ s1) & m in dom (sx ^ s1) & n < m implies (sx ^ s1) /. n <= (sx ^ s1) /. m )
assume that
A8: n in dom (sx ^ s1) and
A9: m in dom (sx ^ s1) and
A10: n < m ; :: thesis: (sx ^ s1) /. n <= (sx ^ s1) /. m
per cases ( n in dom sx or ex k being Nat st
( k in dom s1 & n = (len sx) + k ) )
by ;
suppose n in dom sx ; :: thesis: (sx ^ s1) /. n <= (sx ^ s1) /. m
then n in Seg 1 by FINSEQ_1:38;
then A11: n = 1 by ;
then (sx ^ s1) . n = x by FINSEQ_1:41;
then A12: (sx ^ s1) /. n = x by ;
(sx ^ s1) /. m in C
proof
m in Seg (len (sx ^ s1)) by ;
then A13: m <= len (sx ^ s1) by FINSEQ_1:1;
A14: len sx < m by ;
(sx ^ s1) . m = s1 . (m - (len sx)) by ;
then A15: (sx ^ s1) . m = s1 . (m - 1) by FINSEQ_1:40;
(len sx) + (len s1) = len (sx ^ s1) by FINSEQ_1:22;
then 1 + (len s1) = len (sx ^ s1) by FINSEQ_1:40;
then len s1 = (len (sx ^ s1)) - 1 ;
then A16: m - 1 <= len s1 by ;
not m is zero by A10;
then reconsider m1 = m - 1 as Nat by CHORD:1;
1 < m1 + 1 by ;
then 1 <= m1 by NAT_1:8;
then m1 in Seg (len s1) by ;
then m1 in dom s1 by FINSEQ_1:def 3;
then (sx ^ s1) . m in rng s1 by ;
hence (sx ^ s1) /. m in C by ; :: thesis: verum
end;
hence (sx ^ s1) /. n <= (sx ^ s1) /. m by ; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom s1 & n = (len sx) + k ) ; :: thesis: (sx ^ s1) /. n <= (sx ^ s1) /. m
then consider k being Nat such that
A17: ( k in dom s1 & n = (len sx) + k ) ;
(sx ^ s1) . n = s1 . k by ;
then (sx ^ s1) /. n = s1 . k by ;
then A18: (sx ^ s1) /. n = s1 /. k by ;
A19: ( m in dom sx or ex l being Nat st
( l in dom s1 & m = (len sx) + l ) ) by ;
not m in dom sx then consider l being Nat such that
A21: ( l in dom s1 & m = (len sx) + l ) by A19;
(sx ^ s1) . m = s1 . l by ;
then (sx ^ s1) /. m = s1 . l by ;
then A22: (sx ^ s1) /. m = s1 /. l by ;
k < l by ;
then s1 /. k <= s1 /. l by A17, A21, A5;
hence (sx ^ s1) /. n <= (sx ^ s1) /. m by ; :: thesis: verum
end;
end;
end;
then sx ^ s1 is weakly-ascending ;
hence sx ^ s1 is B -asc_ordering by A6, A7; :: thesis: verum