let p be FinSequence; for x being object
for A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
let x be object ; for A being set holds (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
let A be set ; (p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
set r = (p ^ <*x*>) - A;
set q = <*x*> - A;
set t = p ^ <*x*>;
A1: len (p ^ <*x*>) =
(len p) + (len <*x*>)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:40
;
A2:
now for k being Nat st k in dom (<*x*> - A) holds
((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k
(p ^ <*x*>) " A c= dom (p ^ <*x*>)
by RELAT_1:132;
then A3:
(p ^ <*x*>) " A c= Seg (len (p ^ <*x*>))
by FINSEQ_1:def 3;
set S =
(Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A);
set s =
Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
let k be
Nat;
( k in dom (<*x*> - A) implies ((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . k )A4:
(Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>))
by XBOOLE_1:36;
assume A5:
k in dom (<*x*> - A)
;
((p ^ <*x*>) - A) . ((len (p - A)) + k) = (<*x*> - A) . kthen A6:
not
x in A
by Lm7, RELAT_1:38;
then A7:
<*x*> - A = <*x*>
by Lm6;
then A8:
dom (<*x*> - A) = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then A9:
k = 1
by A5, TARSKI:def 1;
A10:
p " A = (p ^ <*x*>) " A
A23:
dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))))
by FINSEQ_1:def 3;
len (p ^ <*x*>) in Seg (len (p ^ <*x*>))
by A1, FINSEQ_1:4;
then
len (p ^ <*x*>) in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)
by A21, XBOOLE_0:def 5;
then
len (p ^ <*x*>) in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A4, FINSEQ_1:def 13;
then consider y being
object such that A24:
y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
and A25:
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . y = len (p ^ <*x*>)
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A24;
A26:
(len (p - A)) + k =
((len p) - (card (p " A))) + k
by Th57
.=
((len p) + 1) - (card ((p ^ <*x*>) " A))
by A9, A10
.=
((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A))
by FINSEQ_1:39
.=
(len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A))
by FINSEQ_1:22
.=
len ((p ^ <*x*>) - A)
by Th57
;
A27:
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) =
card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))
by Th37, XBOOLE_1:36
.=
(card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A))
by A3, CARD_2:44
.=
(len (p ^ <*x*>)) - (card (p " A))
by A10, FINSEQ_1:57
.=
((len p) - (card (p " A))) + k
by A1, A9
.=
len ((p ^ <*x*>) - A)
by A26, Th57
;
then A28:
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p - A)) + 1
by A5, A8, A26, TARSKI:def 1;
then A29:
len ((p ^ <*x*>) - A) in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A27, A23, FINSEQ_1:4;
A30:
now not y <> len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))A31:
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A27, A29, FUNCT_1:def 3;
reconsider w =
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))) as
Element of
NAT by A31;
w in (Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)
by A4, A31, FINSEQ_1:def 13;
then A32:
w in Seg (len (p ^ <*x*>))
by XBOOLE_0:def 5;
assume A33:
y <> len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
;
contradictionA34:
y in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))))
by A24, FINSEQ_1:def 3;
then
y <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by FINSEQ_1:1;
then A35:
y < len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A33, XXREAL_0:1;
1
<= y
by A34, FINSEQ_1:1;
then
len (p ^ <*x*>) < w
by A4, A25, A35, FINSEQ_1:def 13;
hence
contradiction
by A32, FINSEQ_1:1;
verum end;
dom (p ^ <*x*>) = Seg (len (p ^ <*x*>))
by FINSEQ_1:def 3;
hence ((p ^ <*x*>) - A) . ((len (p - A)) + k) =
(p ^ <*x*>) . (len (p ^ <*x*>))
by A26, A27, A28, A23, A25, A30, FINSEQ_1:4, FUNCT_1:13
.=
x
by A1, FINSEQ_1:42
.=
(<*x*> - A) . k
by A7, A9, FINSEQ_1:def 8
;
verum end;
A36:
now for k being Nat st k in dom (p - A) holds
((p ^ <*x*>) - A) . k = (p - A) . kA37:
(
x in A implies
(p ^ <*x*>) " A = (p " A) \/ {((len p) + 1)} )
(p ^ <*x*>) " A c= dom (p ^ <*x*>)
by RELAT_1:132;
then A48:
(p ^ <*x*>) " A c= Seg (len (p ^ <*x*>))
by FINSEQ_1:def 3;
A49:
( not
x in A implies
(p ^ <*x*>) " A = p " A )
set s2 =
Sgm ((Seg (len p)) \ (p " A));
set s1 =
Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A));
let k be
Nat;
( k in dom (p - A) implies ((p ^ <*x*>) - A) . k = (p - A) . k )A57:
dom p = Seg (len p)
by FINSEQ_1:def 3;
(Seg (len p)) /\ {((len p) + 1)} = {}
then A67:
Seg (len p) misses {((len p) + 1)}
;
p " A c= dom p
by RELAT_1:132;
then A69:
p " A c= Seg (len p)
by FINSEQ_1:def 3;
len (Sgm ((Seg (len p)) \ (p " A))) =
card ((Seg (len p)) \ (p " A))
by Th37, XBOOLE_1:36
.=
(card (Seg (len p))) - (card (p " A))
by A69, CARD_2:44
;
then A70:
len (Sgm ((Seg (len p)) \ (p " A))) = (len p) - (card (p " A))
by FINSEQ_1:57;
(Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A) c= Seg (len (p ^ <*x*>))
by XBOOLE_1:36;
then A71:
rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) c= Seg (len (p ^ <*x*>))
by FINSEQ_1:def 13;
A72:
(Seg (len p)) \ (p " A) c= Seg (len p)
by XBOOLE_1:36;
then A73:
rng (Sgm ((Seg (len p)) \ (p " A))) c= Seg (len p)
by FINSEQ_1:def 13;
assume
k in dom (p - A)
;
((p ^ <*x*>) - A) . k = (p - A) . kthen A74:
k in dom (Sgm ((Seg (len p)) \ (p " A)))
by A57, FUNCT_1:11;
then
(Sgm ((Seg (len p)) \ (p " A))) . k in rng (Sgm ((Seg (len p)) \ (p " A)))
by FUNCT_1:def 3;
then
(Sgm ((Seg (len p)) \ (p " A))) . k in Seg (len p)
by A73;
then A75:
(Sgm ((Seg (len p)) \ (p " A))) . k in dom p
by FINSEQ_1:def 3;
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) =
card ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))
by Th37, XBOOLE_1:36
.=
(card (Seg (len (p ^ <*x*>)))) - (card ((p ^ <*x*>) " A))
by A48, CARD_2:44
;
then A76:
len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) = (len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A))
by FINSEQ_1:57;
A77:
dom (Sgm ((Seg (len p)) \ (p " A))) c= dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
proof
<*x*> " A c= dom <*x*>
by RELAT_1:132;
then
<*x*> " A c= {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then A78:
(
<*x*> " A = {} or
<*x*> " A = {1} )
by ZFMISC_1:33;
let y be
object ;
TARSKI:def 3 ( not y in dom (Sgm ((Seg (len p)) \ (p " A))) or y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) )
A79:
card (p " A) <= (card (p " A)) + 1
by NAT_1:12;
assume A80:
y in dom (Sgm ((Seg (len p)) \ (p " A)))
;
y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
then reconsider l =
y as
Element of
NAT ;
A81:
y in Seg (len (Sgm ((Seg (len p)) \ (p " A))))
by A80, FINSEQ_1:def 3;
then
l <= (len p) - (card (p " A))
by A70, FINSEQ_1:1;
then
l + (card (p " A)) <= len p
by XREAL_1:19;
then A82:
(l + (card (p " A))) + 1
<= len (p ^ <*x*>)
by A1, XREAL_1:7;
card ((p ^ <*x*>) " A) = (card (p " A)) + (card (<*x*> " A))
by Th55;
then
l + (card ((p ^ <*x*>) " A)) <= l + ((card (p " A)) + 1)
by A78, A79, CARD_1:30, XREAL_1:7;
then
l + (card ((p ^ <*x*>) " A)) <= len (p ^ <*x*>)
by A82, XXREAL_0:2;
then A83:
l <= len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A76, XREAL_1:19;
1
<= l
by A81, FINSEQ_1:1;
then
l in Seg (len (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))))
by A83, FINSEQ_1:1;
hence
y in dom (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by FINSEQ_1:def 3;
verum
end; then
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in rng (Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A)))
by A74, FUNCT_1:def 3;
then
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k in Seg (len (p ^ <*x*>))
by A71;
then reconsider l =
(Sgm ((Seg (len (p ^ <*x*>))) \ ((p ^ <*x*>) " A))) . k as
Element of
NAT ;
dom (p ^ <*x*>) = Seg (len (p ^ <*x*>))
by FINSEQ_1:def 3;
then A84:
((p ^ <*x*>) - A) . k = (p ^ <*x*>) . l
by A74, A77, FUNCT_1:13;
(len p) + 1
in Seg ((len p) + 1)
by FINSEQ_1:4;
then A85:
{((len p) + 1)} c= Seg ((len p) + 1)
by ZFMISC_1:31;
(p - A) . k = p . ((Sgm ((Seg (len p)) \ (p " A))) . k)
by A57, A74, FUNCT_1:13;
hence
((p ^ <*x*>) - A) . k = (p - A) . k
by A75, A86, A84, FINSEQ_1:def 7;
verum end;
len ((p ^ <*x*>) - A) =
(len (p ^ <*x*>)) - (card ((p ^ <*x*>) " A))
by Th57
.=
((len p) + (len <*x*>)) - (card ((p ^ <*x*>) " A))
by FINSEQ_1:22
.=
((len p) + (len <*x*>)) - ((card (p " A)) + (card (<*x*> " A)))
by Th55
.=
(((len p) - (card (p " A))) + (len <*x*>)) + (- (card (<*x*> " A)))
.=
((len (p - A)) + (len <*x*>)) + (- (card (<*x*> " A)))
by Th57
.=
(len (p - A)) + ((len <*x*>) - (card (<*x*> " A)))
.=
(len (p - A)) + (len (<*x*> - A))
by Th57
;
hence
(p ^ <*x*>) - A = (p - A) ^ (<*x*> - A)
by A36, A2, Th36; verum