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
A3: product f c= Funcs (dom f),(Union f) by FUNCT_6:10;
card (dom f) in card T by A1, CLASSES2:1;
then card (rng f) in card T by CARD_2:80, ORDINAL1:22;
then rng f in T by A2, CLASSES1:2;
then union (rng f) in T by CLASSES2:65;
then Union f in T by CARD_3:def 4;
then Funcs (dom f),(Union f) in T by A1, CLASSES2:67;
hence product f in T by A3, CLASSES1:def 1; :: thesis: verum