let X be non empty set ; :: thesis: for t being INT-Expression of X holds
( t + (. 0 ,X) = t & t (#) (. 1,X) = t )
let t be INT-Expression of X; :: thesis: ( t + (. 0 ,X) = t & t (#) (. 1,X) = t )

now

let s be Element of Funcs X,INT ; :: thesis: (t + (. 0 ,X)) . s = t . s
A1: (. 0 ,X) . s = 0 by FUNCOP_1:13;
dom (t + (. 0 ,X)) = Funcs X,INT by FUNCT_2:def 1;
hence (t + (. 0 ,X)) . s = (t . s) + ((. 0 ,X) . s) by VALUED_1:def 1
.= t . s by A1 ;
:: thesis: verum

end;

hence t + (. 0 ,X) = t by FUNCT_2:113; :: thesis: t (#) (. 1,X) = t

now

let s be Element of Funcs X,INT ; :: thesis: (t (#) (. 1,X)) . s = t . s
dom (t (#) (. 1,X)) = Funcs X,INT by FUNCT_2:def 1;
hence (t (#) (. 1,X)) . s = (t . s) * ((. 1,X) . s) by VALUED_1:def 4
.= (t . s) * 1 by FUNCOP_1:13
.= t . s ;
:: thesis: verum

end;

hence t (#) (. 1,X) = t by FUNCT_2:113; :: thesis: verum