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

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