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) )

A4: dom t1 = X by FUNCT_2:def 1;

A5: dom t2 = X by FUNCT_2:def 1;

A6: dom (t1 + t2) = (dom t1) /\ (dom t2) by VALUED_1:def 1;

hence ( ti = t1 + t2 implies for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) by A4, A5, VALUED_1:def 1; :: thesis: ( ( for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) implies ti = t1 + t2 )

A7: dom ti = X by FUNCT_2:def 1;

assume for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ; :: thesis: ti = t1 + t2

then for s being object st s in X holds

ti . s = (t1 . s) + (t2 . s) ;

hence ti = t1 + t2 by A6, A4, A5, A7, VALUED_1:def 1; :: thesis: verum

A4: dom t1 = X by FUNCT_2:def 1;

A5: dom t2 = X by FUNCT_2:def 1;

A6: dom (t1 + t2) = (dom t1) /\ (dom t2) by VALUED_1:def 1;

hence ( ti = t1 + t2 implies for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) by A4, A5, VALUED_1:def 1; :: thesis: ( ( for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ) implies ti = t1 + t2 )

A7: dom ti = X by FUNCT_2:def 1;

assume for s being Element of X holds ti . s = (t1 . s) + (t2 . s) ; :: thesis: ti = t1 + t2

then for s being object st s in X holds

ti . s = (t1 . s) + (t2 . s) ;

hence ti = t1 + t2 by A6, A4, A5, A7, VALUED_1:def 1; :: thesis: verum