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 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: sx ^ s1 is one-to-one by A1, FINSEQ_3:91;
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 A8, FINSEQ_1:25;
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 FINSEQ_1:2, TARSKI:def 1;
then (sx ^ s1) . n = x by FINSEQ_1:41;
then A12: (sx ^ s1) /. n = x by A8, PARTFUN1:def 6;
(sx ^ s1) /. m in C
proof
m in Seg (len (sx ^ s1)) by A9, FINSEQ_1:def 3;
then A13: m <= len (sx ^ s1) by FINSEQ_1:1;
A14: len sx < m by A10, A11, FINSEQ_1:40;
(sx ^ s1) . m = s1 . (m - (len sx)) by A13, A14, FINSEQ_1:24;
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 A13, XREAL_1:9;
not m is zero by A10;
then reconsider m1 = m - 1 as Nat by CHORD:1;
1 < m1 + 1 by A10, A11;
then 1 <= m1 by NAT_1:8;
then m1 in Seg (len s1) by A16, FINSEQ_1:1;
then m1 in dom s1 by FINSEQ_1:def 3;
then (sx ^ s1) . m in rng s1 by A15, FUNCT_1:3;
hence (sx ^ s1) /. m in C by A1, A9, PARTFUN1:def 6; :: thesis: verum
end;
hence (sx ^ s1) /. n <= (sx ^ s1) /. m by A12, A4; :: 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 A17, FINSEQ_1:def 7;
then (sx ^ s1) /. n = s1 . k by A8, PARTFUN1:def 6;
then A18: (sx ^ s1) /. n = s1 /. k by A17, PARTFUN1:def 6;
A19: ( m in dom sx or ex l being Nat st
( l in dom s1 & m = (len sx) + l ) ) by A9, FINSEQ_1:25;
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 A21, FINSEQ_1:def 7;
then (sx ^ s1) /. m = s1 . l by A9, PARTFUN1:def 6;
then A22: (sx ^ s1) /. m = s1 /. l by A21, PARTFUN1:def 6;
k < l by A17, A21, A10, XREAL_1:6;
then s1 /. k <= s1 /. l by A17, A21, A5;
hence (sx ^ s1) /. n <= (sx ^ s1) /. m by A18, A22; :: thesis: verum
end;
end;
end;
then sx ^ s1 is weakly-ascending ;
hence sx ^ s1 is B -asc_ordering by A6, A7; :: thesis: verum