let ti be Function of X,INT; :: thesis: ( ti = t1 - t2 iff for s being Element of X holds ti . s = (t1 . s) - (t2 . s) )
thus ( ti = t1 - t2 implies for s being Element of X holds ti . s = (t1 . s) - (t2 . s) ) by VALUED_1:15; :: thesis: ( ( for s being Element of X holds ti . s = (t1 . s) - (t2 . s) ) implies ti = t1 - t2 )
assume A1: for s being Element of X holds ti . s = (t1 . s) - (t2 . s) ; :: thesis: ti = t1 - t2

A2: now :: thesis: for s being object st s in X holds
ti . s = (t1 - t2) . s

let s be object ; :: thesis: ( s in X implies ti . s = (t1 - t2) . s )
assume A3: s in X ; :: thesis: ti . s = (t1 - t2) . s
hence ti . s = (t1 . s) - (t2 . s) by A1
.= (t1 - t2) . s by A3, VALUED_1:15 ;
:: thesis: verum

end;

thus ti = t1 - t2 by A2; :: thesis: verum