let U be Universe; :: thesis: Funcs U c< U
thus Funcs U c= U :: according to XBOOLE_0:def 8 :: thesis: not Funcs U = U

proof

set FAB = { (Funcs (A,B)) where A, B is Element of U : verum } ;

now :: thesis: for o being object st o in { (Funcs (A,B)) where A, B is Element of U : verum } holds
o in U

let o be object ; :: thesis: ( o in { (Funcs (A,B)) where A, B is Element of U : verum } implies o in U )
assume o in { (Funcs (A,B)) where A, B is Element of U : verum } ; :: thesis: o in U
then consider A, B being Element of U such that
A1: o = Funcs (A,B) ;
thus o in U by A1; :: thesis: verum

end;

then { (Funcs (A,B)) where A, B is Element of U : verum } c= U ;
then union { (Funcs (A,B)) where A, B is Element of U : verum } c= union U by ZFMISC_1:77;
hence Funcs U c= U by CLASSES4:81; :: thesis: verum

end;

{{}} is Element of U by CLASSES2:56, CLASSES2:57;
hence not Funcs U = U by Th2; :: thesis: verum