let V be non empty set ; :: thesis: for f being Function
for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )
let f be Function; :: thesis: for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )
let A, B be set ; :: thesis: ( [[A,B],f] in Maps V implies ( ( B = {} implies A = {} ) & f is Function of A,B ) )
assume [[A,B],f] in Maps V ; :: thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
then consider f' being Element of Funcs V, A', B' being Element of V such that
A1: [[A,B],f] = [[A',B'],f'] and
A2: ( ( B' = {} implies A' = {} ) & f' is Function of A',B' ) by Th4;
( f = f' & A = A' & B = B' ) by A1, Lm1, ZFMISC_1:33;
hence ( ( B = {} implies A = {} ) & f is Function of A,B ) by A2; :: thesis: verum