theorem Th61: :: CLASSES2:61

for X, Y being set
for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs (X,Y) in U )