let V be non empty set ; for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V
let A, B be Element of V; for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V
let f be Function of A,B; ( ( B = {} implies A = {} ) implies [[A,B],f] in Maps V )
assume A1:
( B = {} implies A = {} )
; [[A,B],f] in Maps V
then
f in Funcs V
by Th1;
hence
[[A,B],f] in Maps V
by A1; verum