defpred S_{1}[ 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_{1}[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

( 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

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 ) )

thus a in AB by A1, A4; :: thesis: verum

end;( 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 )

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( 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;( 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

thus a in AB by A1, A4; :: thesis: verum