let U be Universe; :: thesis: Funcs U is U -Class
A1: Funcs U c< U by Th103;

A2: now :: thesis: for x being Element of U holds {[x,x]} in Funcs U

let x be Element of U; :: thesis: {[x,x]} in Funcs U
set FAB = { (Funcs (A,B)) where A, B is Element of U : verum } ;
( id {x} in Funcs ({x},{x}) & Funcs ({x},{x}) in { (Funcs (A,B)) where A, B is Element of U : verum } ) ;
then id {x} in union { (Funcs (A,B)) where A, B is Element of U : verum } by TARSKI:def 4;
hence {[x,x]} in Funcs U by SYSREL:13; :: thesis: verum

end;

A3: { {[x,x]} where x is Element of U : verum } c= Funcs U

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { {[x,x]} where x is Element of U : verum } or o in Funcs U )
assume o in { {[x,x]} where x is Element of U : verum } ; :: thesis: o in Funcs U
then ex x being Element of U st o = {[x,x]} ;
hence o in Funcs U by A2; :: thesis: verum

end;

A4: union { {[x,x]} where x is Element of U : verum } = { [x,x] where x is Element of U : verum }

proof

now :: thesis: for o being object st o in union { {[x,x]} where x is Element of U : verum } holds
o in { [x,x] where x is Element of U : verum }

let o be object ; :: thesis: ( o in union { {[x,x]} where x is Element of U : verum } implies o in { [x,x] where x is Element of U : verum } )
assume o in union { {[x,x]} where x is Element of U : verum } ; :: thesis: o in { [x,x] where x is Element of U : verum }
then consider y being set such that
A5: ( o in y & y in { {[x,x]} where x is Element of U : verum } ) by TARSKI:def 4;
consider x being Element of U such that
A6: y = {[x,x]} by A5;
o = [x,x] by A6, A5, TARSKI:def 1;
hence o in { [x,x] where x is Element of U : verum } ; :: thesis: verum

end;

hence union { {[x,x]} where x is Element of U : verum } c= { [x,x] where x is Element of U : verum } ; :: according to XBOOLE_0:def 10 :: thesis: { [x,x] where x is Element of U : verum } c= union { {[x,x]} where x is Element of U : verum }

now :: thesis: for o being object st o in { [x,x] where x is Element of U : verum } holds
o in union { {[x,x]} where x is Element of U : verum }

let o be object ; :: thesis: ( o in { [x,x] where x is Element of U : verum } implies o in union { {[x,x]} where x is Element of U : verum } )
assume o in { [x,x] where x is Element of U : verum } ; :: thesis: o in union { {[x,x]} where x is Element of U : verum }
then consider x being Element of U such that
A7: o = [x,x] ;
A8: o in {[x,x]} by A7, TARSKI:def 1;
{[x,x]} in { {[x,x]} where x is Element of U : verum } ;
hence o in union { {[x,x]} where x is Element of U : verum } by A8, TARSKI:def 4; :: thesis: verum

end;

hence { [x,x] where x is Element of U : verum } c= union { {[x,x]} where x is Element of U : verum } ; :: thesis: verum

end;

now :: thesis: not Funcs U in U

assume Funcs U in U ; :: thesis: contradiction
then { {[x,x]} where x is Element of U : verum } in U by A3, CLASSES4:13;
then reconsider SU = { [x,x] where x is Element of U : verum } as Element of U by A4, CLASSES2:59;
proj1 SU = U

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: U c= proj1 SU

let o be object ; :: thesis: ( o in proj1 SU implies o in U )
assume o in proj1 SU ; :: thesis: o in U
then consider o9 being object such that
A9: [o,o9] in SU by XTUPLE_0:def 12;
consider x being Element of U such that
A10: [o,o9] = [x,x] by A9;
o = x by A10, XTUPLE_0:1;
hence o in U ; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in U or o in proj1 SU )
assume o in U ; :: thesis: o in proj1 SU
then reconsider x = o as Element of U ;
[x,x] in SU ;
hence o in proj1 SU by XTUPLE_0:def 12; :: thesis: verum

end;

then U is Element of U by CLASSES4:36;
then U in U ;
hence contradiction ; :: thesis: verum

end;

hence Funcs U is U -Class by A1; :: thesis: verum