let F be object ; :: according to TARSKI:def 3 :: thesis: ( not F in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } or F in Membership_Funcs REAL )

assume F in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } ; :: thesis: F in Membership_Funcs REAL

then consider f, g being Function of REAL,REAL such that

A1: F = f and

A2: for x being Real holds f . x = max (0,(min (1,(g . x)))) ;

F in { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } by A1, A2;

hence F in Membership_Funcs REAL by MM4, TARSKI:def 3; :: thesis: verum

assume F in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } ; :: thesis: F in Membership_Funcs REAL

then consider f, g being Function of REAL,REAL such that

A1: F = f and

A2: for x being Real holds f . x = max (0,(min (1,(g . x)))) ;

F in { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } by A1, A2;

hence F in Membership_Funcs REAL by MM4, TARSKI:def 3; :: thesis: verum