let ti be Function of X,INT ; :: thesis: ( ti = f - x 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:3;
hence ( ti = f - x implies for s being Element of X holds ti . s = (f . s) - x ) by VALUED_1:3; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) - x ) implies ti = f - x )
assume A2: for s being Element of X holds ti . s = (f . s) - x ; :: thesis: ti = f - x

now

let s be set ; :: thesis: ( s in dom ti implies ti . s = (f - x) . s )
assume A3: s in dom ti ; :: thesis: ti . s = (f - x) . s
hence ti . s = (f . s) - x by A2
.= (f - x) . s by A1, A3, VALUED_1:3 ;
:: thesis: verum

end;

hence ti = f - x by A1, FUNCT_1:9; :: thesis: verum