let V be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( [[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 ; :: thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
hence ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, Th10; :: thesis: verum