let V be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( B = {} implies A = {} ) implies [[A,B],f] in Maps V )
assume A1: ( B = {} implies A = {} ) ; :: thesis: [[A,B],f] in Maps V
then f in Funcs V by Th1;
hence [[A,B],f] in Maps V by A1; :: thesis: verum