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

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