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 :: thesis: for f being BinOp of D st D in UN holds
f in UN
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:61;
then A2: Funcs ([:D,D:],D) in UN by A1, CLASSES2:61;
f in Funcs ([:D,D:],D) by FUNCT_2:8;
hence f in UN by A2, ORDINAL1:10; :: 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 Th28; :: thesis: verum