let F be Function-yielding Function; :: thesis: for f being set st f in dom (Frege F) holds
f is Function
let f be set ; :: thesis: ( f in dom (Frege F) implies f is Function )
assume f in dom (Frege F) ; :: thesis: f is Function
then f in product (doms F) by PARTFUN1:def 4;
hence f is Function ; :: thesis: verum