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 object ; :: according to TARSKI:def 3 :: thesis: ( 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*>)) ; :: thesis: a in dom ({x} |` p)
then A5: a in dom (p ^ <*y*>) by FUNCT_1:54;
then a in Seg ((len p) + ()) by FINSEQ_1:def 7;
then a in (Seg (len p)) \/ {((len p) + 1)} by ;
then A6: ( a in dom p or a in {((len p) + 1)} ) by ;
A7: (p ^ <*y*>) . a in {x} by ;
reconsider a = a as Element of NAT by A5;
A8: ( (p ^ <*y*>) . ((len p) + 1) = y & not y in {x} ) by ;
then (p ^ <*y*>) . a = p . a by ;
hence a in dom ({x} |` p) by ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ({x} |` p) or a in dom ({x} |` (p ^ <*y*>)) )
assume A9: a in dom ({x} |` p) ; :: thesis: 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 ;
then A12: a in dom (p ^ <*y*>) by ;
A13: p . a in {x} by ;
reconsider a = a as Element of NAT by A9;
(p ^ <*y*>) . a = p . a by ;
hence a in dom ({x} |` (p ^ <*y*>)) by ; :: thesis: verum