consider A, B being non empty finite set ;
take P = PFuncs A,B; :: 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 Th5; :: thesis: not P is empty
thus not P is empty ; :: thesis: verum