let k be Integer; :: thesis: ex f being Function of SCM-Data-Loc ,INT st
for x being Element of SCM-Data-Loc holds f . x = k
defpred S₁[ set , set ] means $2 = k;

A1: now

reconsider y = k as Element of INT by INT_1:def 2;
let x be Element of SCM-Data-Loc ; :: thesis: ex y being Element of INT st S₁[x,y]
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

thus ex f being Function of SCM-Data-Loc ,INT st
for x being Element of SCM-Data-Loc holds S₁[x,f . x] from FUNCT_2:sch 3(A1); :: thesis: verum