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:66; :: 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
A5: Funcs (A,B) in { (Funcs (A,B)) where A, B is Element of V : verum } ;
f in Funcs (A,B) by A4, FUNCT_2:8;
hence f in Funcs V by A5, TARSKI:def 4; :: thesis: verum