defpred S1[ object ] means ex f being Function of A,B st
( f = \$1 & f is monotone );
consider AB being set such that
A1: for a being object holds
( a in AB iff ( a in Funcs ( the carrier of A, the carrier of B) & S1[a] ) ) from take AB ; :: thesis: for a being set holds
( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )

thus for a being set holds
( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) :: thesis: verum
proof
let a be set ; :: thesis: ( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )

hereby :: thesis: ( ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) implies a in AB )
assume A2: a in AB ; :: thesis: ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone )

then consider f being Function of A,B such that
A3: ( f = a & f is monotone ) by A1;
take f = f; :: thesis: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone )
thus ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A1, A2, A3; :: thesis: verum
end;
given f being Function of A,B such that A4: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ; :: thesis: a in AB
thus a in AB by A1, A4; :: thesis: verum
end;