theorem :: CLASSES4:15

for UN being Universe
for u, v being Element of UN holds Funcs (u,v) c= { f where f is Function of u,v : verum }