let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom <*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_1:89, Th1;
then ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;
hence <*f,g,h*> . x is set by FINSEQ_1:45; :: thesis: verum