defpred S₁[ set , set ] means ex a being Element of X st
( a = $1 & $2 = H₁(a) );
A1: for x being set st x in X holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in X implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in X ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
then reconsider x = x as Element of X ;
min (r,(f . x)) is Element of REAL by XREAL_0:def 1;
hence ex y being set st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

consider Min being Function of X,REAL such that
A2: for x being set st x in X holds
S₁[x,Min . x] from FUNCT_2:sch 1(A1);
take Min ; :: thesis: for x being set st x in X holds
Min . x = min (r,(f . x))
let x be set ; :: thesis: ( x in X implies Min . x = min (r,(f . x)) )
assume x in X ; :: thesis: Min . x = min (r,(f . x))
then S₁[x,Min . x] by A2;
hence Min . x = min (r,(f . x)) ; :: thesis: verum