let A, B be set ; Funcs (A,B) c= bool [:A,B:]
let x be object ; TARSKI:def 3 ( not x in Funcs (A,B) or x in bool [:A,B:] )
assume
x in Funcs (A,B)
; x in bool [:A,B:]
then consider f being Function such that
A1:
x = f
and
A2:
dom f = A
and
A3:
rng f c= B
by FUNCT_2:def 2;
A4:
f c= [:(dom f),(rng f):]
by RELAT_1:7;
[:(dom f),(rng f):] c= [:A,B:]
by A2, A3, ZFMISC_1:95;
then
f c= [:A,B:]
by A4;
hence
x in bool [:A,B:]
by A1; verum