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 PBOOLE:def 3;
then ex g being Function st
( g = f & dom g = dom (doms F) & ( for x being set st x in dom (doms F) holds
g . x in (doms F) . x ) ) by CARD_3:def 5;
hence f is Function ; :: thesis: verum