let ti be Function of X,INT ; :: thesis: ( ti = f * x iff for s being Element of X holds ti . s = (f . s) * x )
A8: dom (f * x) = dom f by VALUED_1:def 5;
A9: dom f = X by FUNCT_2:def 1;
hence ( ti = f * x implies for s being Element of X holds ti . s = (f . s) * x ) by A8, VALUED_1:def 5; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) * x ) implies ti = f * x )
A10: dom ti = X by FUNCT_2:def 1;
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 A8;
hence ti = f * x by A8, A9, A10, VALUED_1:def 5; :: thesis: verum