let ti be Function of X, INT ; :: thesis: ( ti = f * x iff for s being Element of X holds ti . s = (f . s) * x )
A1: ( dom (f * x) = dom f & dom f = X & dom ti = X ) by FUNCT_2:def 1, VALUED_1:def 5;
hence ( ti = f * x implies for s being Element of X holds ti . s = (f . s) * x ) by VALUED_1:def 5; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) * x ) implies ti = f * x )
assume for s being Element of X holds ti . s = (f . s) * x ; :: thesis: ti = f * x
then for s being set st s in dom (f * x) holds
ti . s = x * (f . s) by A1;
hence ti = f * x by A1, VALUED_1:def 5; :: thesis: verum