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