A1: dom (t + (. i,X)) = Funcs X,INT by FUNCT_2:def 1;

A2: now

let a be set ; :: 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) by FUNCOP_1:13 ; :: 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