the ZeroF of L is Element of the carrier of L null (dom f) ;
then reconsider z1 = the ZeroF of L as Element of the carrier of L \/ (dom f) by TARSKI:def 3;
the OneF of L is Element of the carrier of L null (dom f) ;
then reconsider o1 = the OneF of L as Element of the carrier of L \/ (dom f) by TARSKI:def 3;
A1: dom the adicity of L = the carrier of L \ { the OneF of L} by FUNCT_2:def 1;
dom ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) = ((dom f) \ { the OneF of L}) \/ ( the carrier of L \ { the OneF of L}) by FUNCT_4:def 1, A1
.= ((dom f) \/ the carrier of L) \ { the OneF of L} by XBOOLE_1:42 ;
then ( dom ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) = ( the carrier of L \/ (dom f)) \ {o1} & rng ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) c= INT ) ;
then (f | ((dom f) \ { the OneF of L})) +* the adicity of L is Element of Funcs ((( the carrier of L \/ (dom f)) \ {o1}),INT) by FUNCT_2:def 2;
then reconsider a11 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L as Function of (( the carrier of L \/ (dom f)) \ {o1}),INT ;
set new = Language-like(# ( the carrier of L \/ (dom f)),z1,o1,a11 #);
reconsider new = Language-like(# ( the carrier of L \/ (dom f)),z1,o1,a11 #) as non empty strict Language-like ;
take new ; :: thesis: ( the adicity of new = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of new = the ZeroF of L & the OneF of new = the OneF of L )
thus ( the adicity of new = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of new = the ZeroF of L & the OneF of new = the OneF of L ) ; :: thesis: verum