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