set A = the non empty finite set ;
take P = PFuncs ( the non empty finite set , the non empty finite set ); :: thesis: ( P is functional & P is finite & not P is empty )
thus P is functional ; :: thesis: ( P is finite & not P is empty )
thus P is finite by Th16; :: thesis: not P is empty
thus not P is empty ; :: thesis: verum