. 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

let a be set ; :: 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 by FUNCOP_1:13
.= (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:9; :: thesis: verum