let S1 be non empty Language-like ; :: thesis:
let f be INT -valued Function; :: thesis:
set S2 = S1 extendWith f;
set L1 = LettersOf S1;
set a1 = the adicity of S1;
set a2 = the adicity of (S1 extendWith f);
set z1 = the ZeroF of S1;
set o1 = the OneF of S1;
set X = (dom f) \ { the OneF of S1};
set C1 = the carrier of S1;
set O1 = OwnSymbolsOf S1;
set L2 = LettersOf (S1 extendWith f);
set f1 = f | (((dom f) \ { the OneF of S1}) \ (dom the adicity of S1));
set SS1 = AllSymbolsOf S1;
the carrier of S1 = ( the carrier of S1 \ { the OneF of S1}) \/ ({ the OneF of S1} null the carrier of S1)
.= (dom the adicity of S1) \/ { the OneF of S1} by FUNCT_2:def 1 ;
then f | (((dom f) \ { the OneF of S1}) \ (dom the adicity of S1)) = f | ((dom f) \ the carrier of S1) by XBOOLE_1:41;
then A1: (f | ((dom f) \ the carrier of S1)) \/ the adicity of S1 = (f | ((dom f) \ { the OneF of S1})) +* the adicity of S1 by FOMODEL0:57
.= the adicity of (S1 extendWith f) by Def42 ;
hence LettersOf (S1 extendWith f) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) by FOMODEL0:23; :: thesis:
reconsider Y = (OwnSymbolsOf S1) /\ (dom f) as Subset of the carrier of S1 by XBOOLE_1:1;
thus the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = ( the adicity of S1 | (OwnSymbolsOf S1)) \/ ((f | ((dom f) \ the carrier of S1)) | (OwnSymbolsOf S1)) by A1, FOMODEL0:56
.= ( the adicity of S1 | (OwnSymbolsOf S1)) \/ (f | ((OwnSymbolsOf S1) /\ ((dom f) \ the carrier of S1))) by RELAT_1:71
.= ( the adicity of S1 | (OwnSymbolsOf S1)) \/ (f | (Y \ the carrier of S1))
.= the adicity of S1 | (OwnSymbolsOf S1) ; :: thesis: