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;
then the adicity of S c= the adicity of (S extendWith f) by FUNCT_4:25;
hence S extendWith f is S -extending by A1, Def41; :: thesis: verum