let ti be Function of X,INT; :: thesis: ( ti = f - x iff for s being Element of X holds ti . s = (f . s) - x )
A3: dom ti = X by FUNCT_2:def 1;
A4: 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 VALUED_1:3; :: thesis: ( ( for s being Element of X holds ti . s = (f . s) - x ) implies ti = f - x )
assume A5: for s being Element of X holds ti . s = (f . s) - x ; :: thesis: ti = f - x
A6: now :: thesis: for s being object st s in dom ti holds
ti . s = (f - x) . s
let s be object ; :: thesis: ( s in dom ti implies ti . s = (f - x) . s )
assume A7: s in dom ti ; :: thesis: ti . s = (f - x) . s
hence ti . s = (f . s) - x by A5
.= (f - x) . s by A4, A7, VALUED_1:3 ;
:: thesis: verum
end;
thus ti = f - x by A3, A6; :: thesis: verum