let x be set ; :: thesis: for A being non empty set
for p being FinSequence of A holds dom ({x} | (p ^ <*x*>)) = (dom ({x} | p)) \/ {((len p) + 1)}
let A be non empty set ; :: thesis: for p being FinSequence of A holds dom ({x} | (p ^ <*x*>)) = (dom ({x} | p)) \/ {((len p) + 1)}
let p be FinSequence of A; :: thesis: dom ({x} | (p ^ <*x*>)) = (dom ({x} | p)) \/ {((len p) + 1)}
thus dom ({x} | (p ^ <*x*>)) c= (dom ({x} | p)) \/ {((len p) + 1)} :: according to XBOOLE_0:def 10 :: thesis: (dom ({x} | p)) \/ {((len p) + 1)} c= dom ({x} | (p ^ <*x*>))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ({x} | (p ^ <*x*>)) or a in (dom ({x} | p)) \/ {((len p) + 1)} )
assume a in dom ({x} | (p ^ <*x*>)) ; :: thesis: a in (dom ({x} | p)) \/ {((len p) + 1)}
then A1: ( a in dom (p ^ <*x*>) & (p ^ <*x*>) . a in {x} ) by FUNCT_1:86;
then ( a in Seg ((len p) + (len <*x*>)) & len <*x*> = 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 A2: ( a in dom p or a in {((len p) + 1)} ) by XBOOLE_0:def 3;
reconsider a = a as Element of NAT by A1;
( a in dom p implies (p ^ <*x*>) . a = p . a ) by FINSEQ_1:def 7;
then ( a in dom p implies a in dom ({x} | p) ) by A1, FUNCT_1:86;
hence a in (dom ({x} | p)) \/ {((len p) + 1)} by A2, XBOOLE_0:def 3; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (dom ({x} | p)) \/ {((len p) + 1)} or a in dom ({x} | (p ^ <*x*>)) )
assume A3: a in (dom ({x} | p)) \/ {((len p) + 1)} ; :: thesis: a in dom ({x} | (p ^ <*x*>))
then ( a in dom ({x} | p) or a in {((len p) + 1)} ) by XBOOLE_0:def 3;
then A4: ( ( a in dom p & p . a in {x} ) or ( a in {((len p) + 1)} & a = (len p) + 1 & x in {x} ) ) by FUNCT_1:86, TARSKI:def 1;
len <*x*> = 1 by FINSEQ_1:57;
then A5: ( Seg (len p) = dom p & dom (p ^ <*x*>) = Seg ((len p) + 1) & Seg ((len p) + 1) = (Seg (len p)) \/ {((len p) + 1)} & (p ^ <*x*>) . ((len p) + 1) = x ) by FINSEQ_1:11, FINSEQ_1:59, FINSEQ_1:def 3, FINSEQ_1:def 7;
then A6: a in dom (p ^ <*x*>) by A4, XBOOLE_0:def 3;
reconsider a = a as Element of NAT by A3;
( a in dom p implies (p ^ <*x*>) . a = p . a ) by FINSEQ_1:def 7;
hence a in dom ({x} | (p ^ <*x*>)) by A4, A5, A6, FUNCT_1:86; :: thesis: verum