let x, y be set ; 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 ; for p being FinSequence of A st x <> y holds
dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)
let p be FinSequence of A; ( x <> y implies dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) )
assume A1:
x <> y
; dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)
thus
dom ({x} |` (p ^ <*y*>)) c= dom ({x} |` p)
XBOOLE_0:def 10 dom ({x} |` p) c= dom ({x} |` (p ^ <*y*>))proof
let a be
object ;
TARSKI:def 3 ( not a in dom ({x} |` (p ^ <*y*>)) or a in dom ({x} |` p) )
A2:
len <*y*> = 1
by FINSEQ_1:40;
A3:
Seg (len p) = dom p
by FINSEQ_1:def 3;
assume A4:
a in dom ({x} |` (p ^ <*y*>))
;
a in dom ({x} |` p)
then A5:
a in dom (p ^ <*y*>)
by FUNCT_1:54;
then
a in Seg ((len p) + (len <*y*>))
by FINSEQ_1:def 7;
then
a in (Seg (len p)) \/ {((len p) + 1)}
by A2, FINSEQ_1:9;
then A6:
(
a in dom p or
a in {((len p) + 1)} )
by A3, XBOOLE_0:def 3;
A7:
(p ^ <*y*>) . a in {x}
by A4, FUNCT_1:54;
reconsider a =
a as
Element of
NAT by A5;
A8:
(
(p ^ <*y*>) . ((len p) + 1) = y & not
y in {x} )
by A1, FINSEQ_1:42, TARSKI:def 1;
then
(p ^ <*y*>) . a = p . a
by A7, A6, FINSEQ_1:def 7, TARSKI:def 1;
hence
a in dom ({x} |` p)
by A7, A6, A8, FUNCT_1:54, TARSKI:def 1;
verum
end;
let a be object ; TARSKI:def 3 ( not a in dom ({x} |` p) or a in dom ({x} |` (p ^ <*y*>)) )
assume A9:
a in dom ({x} |` p)
; a in dom ({x} |` (p ^ <*y*>))
then A10:
a in dom p
by FUNCT_1:54;
len <*y*> = 1
by FINSEQ_1:40;
then A11:
dom (p ^ <*y*>) = Seg ((len p) + 1)
by FINSEQ_1:def 7;
( Seg (len p) = dom p & Seg ((len p) + 1) = (Seg (len p)) \/ {((len p) + 1)} )
by FINSEQ_1:9, FINSEQ_1:def 3;
then A12:
a in dom (p ^ <*y*>)
by A10, A11, XBOOLE_0:def 3;
A13:
p . a in {x}
by A9, FUNCT_1:54;
reconsider a = a as Element of NAT by A9;
(p ^ <*y*>) . a = p . a
by A10, FINSEQ_1:def 7;
hence
a in dom ({x} |` (p ^ <*y*>))
by A13, A12, FUNCT_1:54; verum