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

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

thus
ti = f - x
by A3, A6; :: thesis: verumti . 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;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