let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {f1,f2,f3,f4,f5,f6} or x in PFuncs (A,B) )
assume x in {f1,f2,f3,f4,f5,f6} ; :: thesis: x in PFuncs (A,B)
then ( x = f1 or x = f2 or x = f3 or x = f4 or x = f5 or x = f6 ) by ENUMSET1:def 4;
hence x in PFuncs (A,B) by PARTFUN1:45; :: thesis: verum