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

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