let D, D' be non empty set ; :: thesis: for UN being Universe
for f being Function of D,D' st D in UN & D' in UN holds
f in UN
let UN be Universe; :: thesis: for f being Function of D,D' st D in UN & D' in UN holds
f in UN
let f be Function of D,D'; :: thesis: ( D in UN & D' in UN implies f in UN )
assume ( D in UN & D' in UN ) ; :: thesis: f in UN
then A1: Funcs D,D' in UN by CLASSES2:67;
f in Funcs D,D' by FUNCT_2:11;
hence f in UN by A1, GRCAT_1:4; :: thesis: verum