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 A,B
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 A,B
let f be Function of A,B; :: thesis: ( ( B = {} implies A = {} ) implies [[A,B],f] in Maps A,B )
assume ( B = {} implies A = {} ) ; :: thesis: [[A,B],f] in Maps A,B
then ( f in Funcs V & [[A,B],f] in Maps V & Maps A,B = { [[A,B],f'] where f' is Element of Funcs V : [[A,B],f'] in Maps V } ) by Th1, Th5;
hence [[A,B],f] in Maps A,B ; :: thesis: verum