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 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)];
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;
verum end;
hence
not Maps V is empty
; verum