let a be set ; :: according to FACIRC_1:def 3 :: thesis: ( a in dom <*x*> implies not <*x*> . a is pair )
assume a in dom <*x*> ; :: thesis: not <*x*> . a is pair
then <*x*> . a in rng <*x*> by FUNCT_1:def 3;
then <*x*> . a in {x} by FINSEQ_1:39;
hence not <*x*> . a is pair by TARSKI:def 1; :: thesis: verum