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 :: thesis: for s being Element of Funcs (X,INT) holds (t + (. (0,X))) . s = t . s
let s be Element of Funcs (X,INT); :: thesis: (t + (. (0,X))) . s = t . s
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 ;
:: thesis: verum
end;
hence t + (. (0,X)) = t ; :: thesis: t (#) (. (1,X)) = t
now :: thesis: for s being Element of Funcs (X,INT) holds (t (#) (. (1,X))) . s = t . s
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
.= t . s ;
:: thesis: verum
end;
hence t (#) (. (1,X)) = t ; :: thesis: verum