let D be non empty set ; :: thesis: for UN being Universe holds
( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) )
let UN be Universe; :: thesis: ( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) )

now

let f be BinOp of D; :: thesis: ( D in UN implies f in UN )
assume A1: D in UN ; :: thesis: f in UN
then [:D,D:] in UN by CLASSES2:67;
then A2: Funcs [:D,D:],D in UN by A1, CLASSES2:67;
f in Funcs [:D,D:],D by FUNCT_2:11;
hence f in UN by A2, GRCAT_1:4; :: thesis: verum

end;

hence ( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) ) by Th38; :: thesis: verum