let V be non empty set ; 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 ; ( 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 ) )
( 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
;
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
;
ex B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B )
take
B
;
( ( 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;
verum
end;
given A, B being Element of V such that A4:
( ( B = {} implies A = {} ) & f is Function of A,B )
; 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; verum