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 ) by Th1, Th5;

hence [[A,B],f] in Maps (A,B) ; :: thesis: verum

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 ) by Th1, Th5;

hence [[A,B],f] in Maps (A,B) ; :: thesis: verum