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 object st s in dom (f * x) holds
ti . s = x * (f . s) ;
hence ti = f * x by A8, A9, A10, VALUED_1:def 5; :: thesis: verum