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 ; :: 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 ;
hence f in Funcs V by ; :: thesis: verum