let s, t be Function of X,(Free_LMod (X,R)); :: thesis: ( ( for x being Element of X holds s . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) ) & ( for x being Element of X holds t . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) ) implies s = t )
assume that
A3: for x being Element of X holds s . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) and
A4: for x being Element of X holds t . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) ; :: thesis: s = t

now :: thesis: for x being Element of X holds s . x = t . x

let x be Element of X; :: thesis: s . x = t . x
s . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) by A3;
hence s . x = t . x by A4; :: thesis: verum

end;

hence s = t ; :: thesis: verum