let U be Universe; :: thesis: ( proj1 (Maps U) c= [:U,U:] & [:U,U:] \ [:(U \ {{}}),{{}}:] c= proj1 (Maps U) & proj2 (Maps U) = Funcs U )
thus proj1 (Maps U) c= [:U,U:] :: thesis: ( [:U,U:] \ [:(U \ {{}}),{{}}:] c= proj1 (Maps U) & proj2 (Maps U) = Funcs U )

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in proj1 (Maps U) or o in [:U,U:] )
assume o in proj1 (Maps U) ; :: thesis: o in [:U,U:]
then consider o9 being object such that
A1: [o,o9] in Maps U by XTUPLE_0:def 12;
consider A, B being Element of U, f being Element of Funcs U such that
A2: [o,o9] = [[A,B],f] and
( B = {} implies A = {} ) and
f is Function of A,B by A1;
o = [A,B] by A2, XTUPLE_0:1;
hence o in [:U,U:] by ZFMISC_1:def 2; :: thesis: verum

end;

A10: [:U,U:] /\ { [A,B] where A, B is Element of U : ( B = {} implies A = {} ) } c= proj1 (Maps U)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in [:U,U:] /\ { [A,B] where A, B is Element of U : ( B = {} implies A = {} ) } or o in proj1 (Maps U) )
assume A3: o in [:U,U:] /\ { [A,B] where A, B is Element of U : ( B = {} implies A = {} ) } ; :: thesis: o in proj1 (Maps U)
then ( o in [:U,U:] & o in { [A,B] where A, B is Element of U : ( B = {} implies A = {} ) } ) by XBOOLE_0:def 4;
then consider A, B being object such that
A4: A in U and
A5: B in U and
A6: o = [A,B] by ZFMISC_1:def 2;
o in { [A,B] where A, B is Element of U : ( B = {} implies A = {} ) } by A3, XBOOLE_0:def 4;
then consider A9, B9 being Element of U such that
A7: o = [A9,B9] and
A8: ( B9 = {} implies A9 = {} ) ;
A9: ( A = A9 & B = B9 ) by A6, A7, XTUPLE_0:1;
reconsider A = A, B = B as Element of U by A4, A5;
set f = the Function of A,B;
the Function of A,B is Element of Funcs U by ENS_1:1, A8, A9;
then [[A,B], the Function of A,B] in Maps U by A8, A9;
hence o in proj1 (Maps U) by A6, XTUPLE_0:def 12; :: thesis: verum

end;

[:U,U:] /\ ([:U,U:] \ [:(U \ {{}}),{{}}:]) = ([:U,U:] /\ [:U,U:]) \ [:(U \ {{}}),{{}}:] by XBOOLE_1:49;
hence [:U,U:] \ [:(U \ {{}}),{{}}:] c= proj1 (Maps U) by A10, Th1; :: thesis: proj2 (Maps U) = Funcs U
proj2 (Maps U) = Funcs U

proof

thus proj2 (Maps U) c= Funcs U :: according to XBOOLE_0:def 10 :: thesis: Funcs U c= proj2 (Maps U)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in proj2 (Maps U) or o in Funcs U )
assume o in proj2 (Maps U) ; :: thesis: o in Funcs U
then consider o9 being object such that
A11: [o9,o] in Maps U by XTUPLE_0:def 13;
consider A, B being Element of U, f being Element of Funcs U such that
A12: [o9,o] = [[A,B],f] and
( B = {} implies A = {} ) and
f is Function of A,B by A11;
o = f by A12, XTUPLE_0:1;
hence o in Funcs U ; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Funcs U or o in proj2 (Maps U) )
assume A13: o in Funcs U ; :: thesis: o in proj2 (Maps U)
then consider A, B being Element of U such that
A14: ( B = {} implies A = {} ) and
A15: o is Function of A,B by ENS_1:1;
reconsider f = o as Function of A,B by A15;
[[A,B],f] in Maps U by A14, A13;
hence o in proj2 (Maps U) by XTUPLE_0:def 13; :: thesis: verum

end;

hence proj2 (Maps U) = Funcs U ; :: thesis: verum