let T be Universe; :: thesis: for f being Function st dom f in T & rng f c= T holds
product f in T
let f be Function; :: thesis: ( dom f in T & rng f c= T implies product f in T )
assume that
A1: dom f in T and
A2: rng f c= T ; :: thesis: product f in T
card (dom f) in card T by A1, CLASSES2:1;
then card (rng f) in card T by CARD_2:61, ORDINAL1:12;
then rng f in T by A2, CLASSES1:1;
then union (rng f) in T by CLASSES2:59;
then Union f in T by CARD_3:def 4;
then ( product f c= Funcs ((dom f),(Union f)) & Funcs ((dom f),(Union f)) in T ) by A1, CLASSES2:61, FUNCT_6:1;
hence product f in T by CLASSES1:def 1; :: thesis: verum