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

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