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

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