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