let x, y be set ; :: thesis: for A being non empty set
for p being FinSequence of A st x <> y holds
dom ({x} | (p ^ <*y*>)) = dom ({x} | p)
let A be non empty set ; :: thesis: for p being FinSequence of A st x <> y holds
dom ({x} | (p ^ <*y*>)) = dom ({x} | p)
let p be FinSequence of A; :: thesis: ( x <> y implies dom ({x} | (p ^ <*y*>)) = dom ({x} | p) )
assume A1:
x <> y
; :: thesis: dom ({x} | (p ^ <*y*>)) = dom ({x} | p)
thus
dom ({x} | (p ^ <*y*>)) c= dom ({x} | p)
:: according to XBOOLE_0:def 10 :: thesis: dom ({x} | p) c= dom ({x} | (p ^ <*y*>))proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in dom ({x} | (p ^ <*y*>)) or a in dom ({x} | p) )
assume
a in dom ({x} | (p ^ <*y*>))
;
:: thesis: a in dom ({x} | p)
then A2:
(
a in dom (p ^ <*y*>) &
(p ^ <*y*>) . a in {x} )
by FUNCT_1:86;
then
(
a in Seg ((len p) + (len <*y*>)) &
len <*y*> = 1 )
by FINSEQ_1:57, FINSEQ_1:def 7;
then
(
a in (Seg (len p)) \/ {((len p) + 1)} &
Seg (len p) = dom p )
by FINSEQ_1:11, FINSEQ_1:def 3;
then A3:
(
a in dom p or
a in {((len p) + 1)} )
by XBOOLE_0:def 3;
reconsider a =
a as
Element of
NAT by A2;
A4:
(
(p ^ <*y*>) . ((len p) + 1) = y & not
y in {x} )
by A1, FINSEQ_1:59, TARSKI:def 1;
then
(p ^ <*y*>) . a = p . a
by A2, A3, FINSEQ_1:def 7, TARSKI:def 1;
hence
a in dom ({x} | p)
by A2, A3, A4, FUNCT_1:86, TARSKI:def 1;
:: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ({x} | p) or a in dom ({x} | (p ^ <*y*>)) )
assume A5:
a in dom ({x} | p)
; :: thesis: a in dom ({x} | (p ^ <*y*>))
then A6:
( a in dom p & p . a in {x} )
by FUNCT_1:86;
len <*y*> = 1
by FINSEQ_1:57;
then
( Seg (len p) = dom p & dom (p ^ <*y*>) = Seg ((len p) + 1) & Seg ((len p) + 1) = (Seg (len p)) \/ {((len p) + 1)} & (p ^ <*y*>) . ((len p) + 1) = y )
by FINSEQ_1:11, FINSEQ_1:59, FINSEQ_1:def 3, FINSEQ_1:def 7;
then A7:
a in dom (p ^ <*y*>)
by A6, XBOOLE_0:def 3;
reconsider a = a as Element of NAT by A5;
(p ^ <*y*>) . a = p . a
by A6, FINSEQ_1:def 7;
hence
a in dom ({x} | (p ^ <*y*>))
by A6, A7, FUNCT_1:86; :: thesis: verum