let A, B be set ; :: thesis: Funcs (A,B) c= bool [:A,B:]
let x be object ; :: 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 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; :: thesis: verum