let g be Function of REAL,REAL; :: thesis: { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } c= Membership_Funcs REAL
let f0 be object ; :: according to TARSKI:def 3 :: thesis: ( not f0 in { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } or f0 in Membership_Funcs REAL )
assume f0 in { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } ; :: thesis: f0 in Membership_Funcs REAL
then consider f being Function of REAL,REAL such that
A1: f0 = f and
A2: for x being Real holds f . x = max (0,(min (1,(g . x)))) ;
rng f c= [.0,1.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [.0,1.] )
assume y in rng f ; :: thesis: y in [.0,1.]
then consider x being object such that
B2: x in REAL and
B3: y = f . x by FUNCT_2:11;
reconsider x = x as Real by B2;
B4: y = max (0,(min (1,(g . x)))) by A2, B3;
min (1,(g . x)) <= 1 by XXREAL_0:17;
then ( 0 <= max (0,(min (1,(g . x)))) & max (0,(min (1,(g . x)))) <= 1 ) by XXREAL_0:28, XXREAL_0:25;
hence y in [.0,1.] by B4; :: thesis: verum

end;

then f is [.0,1.] -valued ;
hence f0 in Membership_Funcs REAL by Def1, A1; :: thesis: verum