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) )
A1: dom t1 = X by FUNCT_2:def 1;
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 )
A2: dom ti = X by FUNCT_2:def 1;
assume A3: for s being Element of X holds ti . s = (t1 . s) - (t2 . s) ; :: thesis: ti = t1 - t2

A4: now

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

end;

A6: dom t2 = X by FUNCT_2:def 1;
dom (t1 - t2) = (dom t1) /\ (dom t2) by VALUED_1:12;
hence ti = t1 - t2 by A1, A6, A2, A4, FUNCT_1:2; :: thesis: verum