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