let U be Universe; :: thesis: Maps U c= U
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Maps U or o in U )
assume o in Maps U ; :: thesis: o in U
then consider A, B being Element of U, f being Element of Funcs U such that
A1: o = [[A,B],f] and
( B = {} implies A = {} ) and
A2: f is Function of A,B ;
f in bool [:A,B:] by A2;
then f in U by CLASSES4:13;
hence o in U by A1, CLASSES2:58; :: thesis: verum