let ti be Function of X,INT ; :: thesis: ( ti = x + f 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 2;
hence ( ti = f + x implies for s being Element of X holds ti . s = (f . s) + x ) by VALUED_1:def 2; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) + x ) implies ti = x + f )
assume for s being Element of X holds ti . s = (f . s) + x ; :: thesis: ti = x + f
then for s being set st s in X holds
ti . s = x + (f . s) ;
hence ti = x + f by A1, VALUED_1:def 2; :: thesis: verum