let V be non empty set ; :: thesis: for f being set holds
( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )
let f be set ; :: thesis: ( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )
set F = { (Funcs A,B) where A, B is Element of V : verum } ;
thus ( f in Funcs V implies ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) ) :: thesis: ( ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) implies f in Funcs V )

proof

assume f in Funcs V ; :: thesis: ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B )
then consider C being set such that
A1: f in C and
A2: C in { (Funcs A,B) where A, B is Element of V : verum } by TARSKI:def 4;
consider A, B being Element of V such that
A3: C = Funcs A,B by A2;
take A ; :: thesis: ex B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B )
take B ; :: thesis: ( ( B = {} implies A = {} ) & f is Function of A,B )
thus ( ( B = {} implies A = {} ) & f is Function of A,B ) by A1, A3, FUNCT_2:121; :: thesis: verum

end;

given A, B being Element of V such that A4: ( ( B = {} implies A = {} ) & f is Function of A,B ) ; :: thesis: f in Funcs V
( f in Funcs A,B & Funcs A,B in { (Funcs A,B) where A, B is Element of V : verum } ) by A4, FUNCT_2:11;
hence f in Funcs V by TARSKI:def 4; :: thesis: verum