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

A9: 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 A8, VALUED_1:def 4
.= i * (t . a) by FUNCOP_1:13 ; :: thesis: verum

end;

. i,X is INT-Expression of A,f by Def22;
then A10: t (#) (. i,X) is INT-Expression of A,f by Def22;
dom t = Funcs X,INT by FUNCT_2:def 1;
hence t * i is INT-Expression of A,f by A10, A8, A9, VALUED_1:def 5; :: thesis: verum