let U be Universe; :: thesis: for X, Y being non empty set st Funcs (X,Y) is Element of U holds
X is Element of U
let X, Y be non empty set ; :: thesis: ( Funcs (X,Y) is Element of U implies X is Element of U )
assume A1: Funcs (X,Y) is Element of U ; :: thesis: X is Element of U
set y = the Element of Y;
A2: [:X,{ the Element of Y}:] c= union (Funcs (X,Y)) by Th5;
union (Funcs (X,Y)) in U by A1, CLASSES2:59;
then [:X,{ the Element of Y}:] is Element of U by A2, CLASSES4:13;
hence X is Element of U by CLASSES4:40; :: thesis: verum