let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 <*f,g*> or <*f,g*> . x is set )
assume x in dom <*f,g*> ; :: thesis: <*f,g*> . x is set
then x in {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence <*f,g*> . x is set by FINSEQ_1:61; :: thesis: verum