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 by FUNCT_2:def 1;
dom (f + x) = dom f by VALUED_1:def 2;
hence ( ti = f + x implies for s being Element of X holds ti . s = (f . s) + x ) by A1, VALUED_1:def 2; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) + x ) implies ti = x + f )
A2: dom ti = X by FUNCT_2:def 1;
assume for s being Element of X holds ti . s = (f . s) + x ; :: thesis: ti = x + f
then for s being object st s in X holds
ti . s = x + (f . s) ;
hence ti = x + f by A1, A2, VALUED_1:def 2; :: thesis: verum