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

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