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

hence sx ^ s1 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

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

then
sx ^ s1 is weakly-ascending
;
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

end;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;

end;

( 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

end;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

hence
(sx ^ s1) /. n <= (sx ^ s1) /. m
by A12, A4; :: thesis: verum
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;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

suppose
ex k being Nat st

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

( 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

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;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

proof

then consider l being Nat such that
assume
m in dom sx
; :: thesis: contradiction

then m in Seg (len sx) by FINSEQ_1:def 3;

then m in Seg 1 by FINSEQ_1:40;

then A20: m = 1 by FINSEQ_1:2, TARSKI:def 1;

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

then 1 <= k by FINSEQ_1:1;

then 1 < k + 1 by NAT_1:13;

hence contradiction by A20, A10, A17, FINSEQ_1:40; :: thesis: verum

end;then m in Seg (len sx) by FINSEQ_1:def 3;

then m in Seg 1 by FINSEQ_1:40;

then A20: m = 1 by FINSEQ_1:2, TARSKI:def 1;

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

then 1 <= k by FINSEQ_1:1;

then 1 < k + 1 by NAT_1:13;

hence contradiction by A20, A10, A17, FINSEQ_1:40; :: thesis: verum

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

hence sx ^ s1 is B -asc_ordering by A6, A7; :: thesis: verum