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