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:61;
f in Funcs (D,D9) by FUNCT_2:8;
hence f in UN by A1, ORDINAL1:10; :: thesis: verum