defpred S₁[ Element of X, Element of (Free_LMod (X,R))] means $2 = ((ev_ ($1,R)) . f) * ((IotaMap (X,R)) . $1);
A1: for x being Element of X ex y being Element of (Free_LMod (X,R)) st S₁[x,y] ;
consider F being Function of X,(Free_LMod (X,R)) such that
A2: for x being Element of X holds S₁[x,F . x] from FUNCT_2:sch 3(A1);
take F ; :: thesis: for x being Element of X holds F . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x)
let x be Element of X; :: thesis: F . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x)
thus F . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) by A2; :: thesis: verum