let A, B be set ; :: thesis: Funcs A,B c= bool [:A,B:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs A,B or x in bool [:A,B:] )
assume x in Funcs A,B ; :: thesis: x in bool [:A,B:]
then consider f being Function such that
A1: x = f and
A2: ( dom f = A & rng f c= B ) by FUNCT_2:def 2;
A3: f c= [:(dom f),(rng f):] by RELAT_1:21;
[:(dom f),(rng f):] c= [:A,B:] by A2, ZFMISC_1:118;
then f c= [:A,B:] by A3, XBOOLE_1:1;
hence x in bool [:A,B:] by A1; :: thesis: verum