. (i,X) is INT-Expression of A,f by Def22;
then - (. (i,X)) is INT-Expression of A,f by Def22;
then A4: t + (- (. (i,X))) is INT-Expression of A,f by Def22;
A5: dom t = Funcs (X,INT) by FUNCT_2:def 1;
A6: dom (t + (- (. (i,X)))) = Funcs (X,INT) by FUNCT_2:def 1;

A7: now :: thesis: for a being object st a in Funcs (X,INT) holds
(t + (- (. (i,X)))) . a = (t - i) . a

let a be object ; :: thesis: ( a in Funcs (X,INT) implies (t + (- (. (i,X)))) . a = (t - i) . a )
assume a in Funcs (X,INT) ; :: thesis: (t + (- (. (i,X)))) . a = (t - i) . a
then reconsider s = a as Element of Funcs (X,INT) ;
thus (t + (- (. (i,X)))) . a = (t . s) + ((- (. (i,X))) . s) by A6, VALUED_1:def 1
.= (t . s) + (- ((. (i,X)) . s)) by VALUED_1:8
.= (t . s) - i
.= (t - i) . a by A5, VALUED_1:3 ; :: thesis: verum

end;

dom (t - i) = dom t by VALUED_1:3;
hence t - i is INT-Expression of A,f by A4, A6, A5, A7, FUNCT_1:2; :: thesis: verum