set FV = { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;

set A = the Element of V;

set A = the Element of V;

now :: thesis: ex m being Element of [:[:V,V:],(bool [: the Element of V, the Element of V:]):] st m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) }

hence
not Maps V is empty
; :: thesis: verumset f = id the Element of V;

take m = [[ the Element of V, the Element of V],(id the Element of V)]; :: thesis: m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) }

A1: ( the Element of V = {} implies the Element of V = {} ) ;

id the Element of V in Funcs V by Th1;

hence m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } by A1; :: thesis: verum

end;take m = [[ the Element of V, the Element of V],(id the Element of V)]; :: thesis: m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) }

A1: ( the Element of V = {} implies the Element of V = {} ) ;

id the Element of V in Funcs V by Th1;

hence m in { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } by A1; :: thesis: verum