set L1 = L;
set a1 = the adicity of L;
set SS1 = AllSymbolsOf L;
set L2 = L extendWith f;
set SS2 = AllSymbolsOf (L extendWith f);
set a2 = the adicity of (L extendWith f);
set X = dom f;
set E1 = TheEqSymbOf L;
set N1 = TheNorSymbOf L;
set E2 = TheEqSymbOf (L extendWith f);
set N2 = TheNorSymbOf (L extendWith f);
reconsider Y = (dom f) \ {(TheNorSymbOf L)} as Subset of (dom f) ;
the adicity of (L extendWith f) = (f | ((dom f) \ {(TheNorSymbOf L)})) +* the adicity of L by Def42;
then dom the adicity of (L extendWith f) = (dom (f | Y)) \/ (dom the adicity of L) by FUNCT_4:def 1;
then A1: (AllSymbolsOf (L extendWith f)) \ {(TheNorSymbOf (L extendWith f))} = Y \/ (dom the adicity of L) by FUNCT_2:def 1
.= Y \/ ((AllSymbolsOf L) \ {(TheNorSymbOf L)}) by FUNCT_2:def 1 ;
reconsider NN1 = {(TheNorSymbOf L)} as non empty Subset of (AllSymbolsOf L) by ZFMISC_1:31;
reconsider NN2 = {(TheNorSymbOf (L extendWith f))} as non empty Subset of (AllSymbolsOf (L extendWith f)) by ZFMISC_1:31;
( NN1 c= AllSymbolsOf L & (AllSymbolsOf L) null (dom f) c= (AllSymbolsOf L) \/ (dom f) ) ;
then reconsider NN11 = NN1 as non empty Subset of ((AllSymbolsOf L) \/ (dom f)) by XBOOLE_1:1;
( AllSymbolsOf (L extendWith f) = NN2 \/ ((AllSymbolsOf (L extendWith f)) \ NN2) & AllSymbolsOf L = NN1 \/ ((AllSymbolsOf L) \ NN1) ) by XBOOLE_1:45;
then AllSymbolsOf (L extendWith f) = (NN2 \/ ((AllSymbolsOf L) \ NN1)) \/ Y by XBOOLE_1:4, A1
.= (NN1 \/ ((AllSymbolsOf L) \ NN1)) \/ Y by Def41
.= NN1 \/ (((AllSymbolsOf L) \ NN1) \/ Y) by XBOOLE_1:4
.= NN11 \/ (((AllSymbolsOf L) \/ (dom f)) \ NN11) by XBOOLE_1:42
.= (AllSymbolsOf L) \/ (dom f) by XBOOLE_1:45 ;
hence for b₁ being set st b₁ = (AllSymbolsOf (L extendWith f)) \+\ ((dom f) \/ (AllSymbolsOf L)) holds
b₁ is empty ; :: thesis: verum