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

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

thus
ti = t1 - t2
by A2; :: thesis: verumti . 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;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