As per @savask's comments

set.mm

@@ -487082,9 +487082,8 @@ its graph has a given second element (that is, function value).
   ${
     nn0difffzod.1 $e |- ( ph -> N e. ZZ ) $.
     nn0difffzod.2 $e |- ( ph -> M e. ( NN0 \ ( 0 ..^ N ) ) ) $.
-    $( Membership in the nonnegative integers, except a half-open range
-       starting from zero, implies inequality.  (Contributed by Thierry Arnoux,
-       20-Feb-2025.) $)
+    $( A nonnegative integer that is not in the half-open range from 0 to ` N `
+       is at least ` N `.  (Contributed by Thierry Arnoux, 20-Feb-2025.) $)
     nn0difffzod $p |- ( ph -> -. M < N ) $=
       ( cc0 cfzo co wcel wn cn0 cz clt wbr eldifbd eldifad wa wi w3a elfzo0z
       biimpri 3expa con3i imnan sylibr imp syl12anc ) ABFCGHZIZJZBKIZCLIZBCMNZJ
@@ -499499,7 +499498,7 @@ such that every prime ideal contains a prime element (this is a
     $}
 
     $d P a b x $.  $d R a b $.  $d S a b x $.  $d a b ph x $.
-    $( The space ` E ` of the univariate polynomials of degree less than ` N `
+    $( The space ` S ` of the univariate polynomials of degree less than ` N `
        forms a vector subspace.  (Contributed by Thierry Arnoux,
        20-Feb-2025.) $)
     ply1degltlss $p |- ( ph -> S e. ( LSubSp ` P ) ) $=
@@ -499583,7 +499582,7 @@ such that every prime ideal contains a prime element (this is a
     ply1gsumz.a $e |- ( ph -> A : ( 0 ..^ N ) --> B ) $.
     ply1gsumz.s $e |- ( ph -> ( P gsum ( A oF ( .s ` P ) F ) ) = Z ) $.
     $( If a polynomial given as a sum of scaled monomials by factors ` A ` is
-       the zero polynomials, then all factors ` A ` are zero.  (Contributed by
+       the zero polynomial, then all factors ` A ` are zero.  (Contributed by
        Thierry Arnoux, 20-Feb-2025.) $)
     ply1gsumz $p |- ( ph -> A = ( ( 0 ..^ N ) X. { .0. } ) ) $=
       ( cfv vj vi cn0 csn cxp cc0 cfzo co cres cco1 ffnd cbs wcel ply1ring eqid
@@ -500237,7 +500236,7 @@ such that every prime ideal contains a prime element (this is a
 
     $d E i n $.  $d F i $.  $d N i k n $.  $d P i k $.  $d P i n $.
     $d R i k $.  $d R i n $.  $d S n $.  $d i n ph $.
-    $( The space ` E ` of the univariate polynomials of degree less than ` N `
+    $( The space ` S ` of the univariate polynomials of degree less than ` N `
        has dimension ` N ` .  (Contributed by Thierry Arnoux, 20-Feb-2025.) $)
     ply1degltdim $p |- ( ph -> ( dim ` E ) = N ) $=
       ( vn cfv co wcel wceq eqid cxr vk vi cldim cc0 cfzo cv1 cmgp cmg cmpt crn