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 + t2) = (dom t1) /\ (dom t2) & dom t1 = X & dom t2 = X & dom ti = X ) by FUNCT_2:def 1, VALUED_1:def 1;
hence ( ti = t1 + t2 implies for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) by VALUED_1:def 1; :: thesis: ( ( for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) implies ti = t1 + t2 )
assume for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ; :: thesis: ti = t1 + t2
then for s being set st s in X holds
ti . s = (t1 . s) + (t2 . s) ;
hence ti = t1 + t2 by A1, VALUED_1:def 1; :: thesis: verum