let B be Subset of A; :: thesis: B is functional
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( x in B implies x is Function )
thus ( x in B implies x is Function ) ; :: thesis: verum