defpred S₁[ 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) & S₁[a] ) ) from XBOOLE_0:sch 1();
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;