defpred S₁[ object , object ] means ex x being Element of X st
( $1 = x & $2 = a * (f . x) );

A: now :: thesis: for o being object st o in X holds
ex y being object st
( y in the carrier of L & S₁[o,y] )

let o be object ; :: thesis: ( o in X implies ex y being object st
( y in the carrier of L & S₁[o,y] ) )
assume o in X ; :: thesis: ex y being object st
( y in the carrier of L & S₁[o,y] )
then reconsider x = o as Element of X ;
thus ex y being object st
( y in the carrier of L & S₁[o,y] ) :: thesis: verum

proof

take y = a * (f . x); :: thesis: ( y in the carrier of L & S₁[o,y] )
thus y in the carrier of L ; :: thesis: S₁[o,y]
thus S₁[o,y] ; :: thesis: verum

end;

end;

consider h being Function of X, the carrier of L such that
B: for x being object st x in X holds
S₁[x,h . x] from FUNCT_2:sch 1(A);
take h ; :: thesis: for x being Element of X holds h . x = a * (f . x)

now :: thesis: for x being Element of X holds h . x = a * (f . x)

let x be Element of X; :: thesis: h . x = a * (f . x)
S₁[x,h . x] by B;
hence h . x = a * (f . x) ; :: thesis: verum

end;

hence for x being Element of X holds h . x = a * (f . x) ; :: thesis: verum