let A be transitive RelStr ; 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; 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; 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; ( 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
; 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
; ( sx ^ s1 = <*x*> ^ s1 & sx ^ s1 is B -asc_ordering )
thus
sx ^ s1 = <*x*> ^ s1
; 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;
( 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
;
(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
;
(sx ^ s1) /. n <= (sx ^ s1) /. mthen
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;
verum
end; hence
(sx ^ s1) /. n <= (sx ^ s1) /. m
by A12, A4;
verum end; suppose
ex
k being
Nat st
(
k in dom s1 &
n = (len sx) + k )
;
(sx ^ s1) /. n <= (sx ^ s1) /. mthen 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;
verum end;
end;
then
sx ^ s1 is weakly-ascending
;
hence
sx ^ s1 is B -asc_ordering
by A6, A7; verum