let a be set ; :: according to FACIRC_1:def 3 :: thesis: ( a in dom <*x,y,z*> implies not <*x,y,z*> . a is pair )

assume a in dom <*x,y,z*> ; :: thesis: not <*x,y,z*> . a is pair

then <*x,y,z*> . a in rng <*x,y,z*> by FUNCT_1:def 3;

then <*x,y,z*> . a in {x,y,z} by FINSEQ_2:128;

hence not <*x,y,z*> . a is pair by ENUMSET1:def 1; :: thesis: verum

assume a in dom <*x,y,z*> ; :: thesis: not <*x,y,z*> . a is pair

then <*x,y,z*> . a in rng <*x,y,z*> by FUNCT_1:def 3;

then <*x,y,z*> . a in {x,y,z} by FINSEQ_2:128;

hence not <*x,y,z*> . a is pair by ENUMSET1:def 1; :: thesis: verum