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 f9 being Element of Funcs V, A9, B9 being Element of V such that
A1: [[A,B],f] = [[A9,B9],f9] and
A2: ( ( B9 = {} implies A9 = {} ) & f9 is Function of A9,B9 ) by Th4;
( f = f9 & A = A9 ) by A1, Lm1, XTUPLE_0:1;
hence ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, A2, Lm1; :: thesis: verum