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

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