set S1 = S;
set S2 = S extendWith f;
set a1 = the adicity of S;
set a2 = the adicity of (S extendWith f);
set o1 = the OneF of S;
A1: ( TheEqSymbOf S = TheEqSymbOf (S extendWith f) & TheNorSymbOf S = TheNorSymbOf (S extendWith f) ) by Def42;
the adicity of (S extendWith f) = (f | ((dom f) \ { the OneF of S})) +* the adicity of S by Def42;
hence for b₁ being non empty strict Language-like st b₁ = S extendWith f holds
b₁ is S -extending by A1, FUNCT_4:25; :: thesis: verum