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;

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 ) }

set 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;

hence not Maps V is empty ; :: thesis: verum