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

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

A2: now :: thesis: for a being object st a in Funcs (X,INT) holds

(t + (. (i,X))) . a = i + (t . a)

. (i,X) is INT-Expression of A,f
by Def22;(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;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

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