A1: dom (t + (. (i,X))) = Funcs (X,INT) by FUNCT_2:def 1;
A2: now :: thesis: for a being object st a in Funcs (X,INT) holds
(t + (. (i,X))) . a = i + (t . a)
let a be object ; :: thesis: ( a in Funcs (X,INT) implies (t + (. (i,X))) . a = i + (t . a) )
assume a in Funcs (X,INT) ; :: thesis: (t + (. (i,X))) . a = i + (t . a)
then reconsider s = a as Element of Funcs (X,INT) ;
thus (t + (. (i,X))) . a = (t . s) + ((. (i,X)) . s) by A1, VALUED_1:def 1
.= i + (t . a) ; :: thesis: verum
end;
. (i,X) is INT-Expression of A,f by Def22;
then A3: t + (. (i,X)) is INT-Expression of A,f by Def22;
dom t = Funcs (X,INT) by FUNCT_2:def 1;
hence i + t is INT-Expression of A,f by A3, A1, A2, VALUED_1:def 2; :: thesis: verum