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 )

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

( 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

given A, B being Element of V such that A4:
( ( B = {} implies A = {} ) & f is Function of A,B )
; :: thesis: f in Funcs V
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;( ( 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

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