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 ) } ;
consider A being Element of V;

now

set f = id A;
take m = [[A,A],(id A)]; :: 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: ( A = {} implies A = {} ) ;
then ( id A in Funcs V & [A,A] in [:V,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