diff --git a/iset.mm b/iset.mm
index b7e1d41fc8..f9d730a9d8 100644
--- a/iset.mm
+++ b/iset.mm
@@ -50496,6 +50496,25 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
       CUHUJTVAUQACUNCRUSUOUTUPUNCDSUNCESUAUBUCUD $.
   $}
 
+  ${
+    $d A a i $.  $d C i $.  $d D a $.  $d M a i $.  $d U a i $.  $d V a i $.
+    $d ph a i $.
+    fnmptfvd.m $e |- ( ph -> M Fn A ) $.
+    fnmptfvd.s $e |- ( i = a -> D = C ) $.
+    fnmptfvd.d $e |- ( ( ph /\ i e. A ) -> D e. U ) $.
+    fnmptfvd.c $e |- ( ( ph /\ a e. A ) -> C e. V ) $.
+    $( A function with a given domain is a mapping defined by its function
+       values.  (Contributed by AV, 1-Mar-2019.) $)
+    fnmptfvd $p |- ( ph -> ( M = ( a e. A |-> C )
+                              <-> A. i e. A ( M ` i ) = D ) ) $=
+      ( cmpt wceq cfv wral wfn wcel eqid cv ralrimiva fnmpt syl syl2anc cbvmptv
+      wb eqfnfv eqcomi a1i fveq1d eqeq2d ralbidv simpr fvmpt2 ralbidva 3bitrd
+      wa ) AGIBCNZOZFUAZGPZVAUSPZOZFBQZVBVAFBDNZPZOZFBQVBDOZFBQAGBRUSBRZUTVEUGJ
+      ACHSZIBQVJAVKIBMUBIBCUSHUSTUCUDFBGUSUHUEAVDVHFBAVCVGVBAVAUSVFUSVFOAVFUSFI
+      BDCKUFUIUJUKULUMAVHVIFBAVABSZURZVGDVBVMVLDESVGDOAVLUNLFBDEVFVFTUOUEULUPUQ
+      $.
+  $}
+
   ${
     $d F x y $.  $d G x y $.  $d A x y $.
     $( Two ways to express the locus of differences between two functions.
@@ -71014,6 +71033,23 @@ of Omniscience (WLPO).
     ( cen wbr cwomni wcel enwomnilem wi ensym syl impbid ) ABCDZAEFZBEFZABGLBAC
     DNMHABIBAGJK $.
 
+  ${
+    $d N f x $.  $d N i x $.  $d i ph x $.
+    nninfdcinf.w $e |- ( ph -> _om e. WOmni ) $.
+    nninfdcinf.n $e |- ( ph -> N e. NN+oo ) $.
+    $( The Weak Limited Principle of Omniscience (WLPO) implies that it is
+       decidable whether an element of ` NN+oo ` equals the point at infinity.
+       (Contributed by Jim Kingdon, 3-Dec-2024.) $)
+    nninfdcinf $p |- ( ph -> DECID N = ( i e. _om |-> 1o ) ) $=
+      ( vx vf com c1o wceq wdc cv cfv wral c2o dcbid cwomni wcel cvv syl eqeq1d
+      cmpt cmap co fveq1 ralbidv wb elexd iswomnimap mpbid wf xnninf 2onn elexi
+      nninff omex elmap sylibr rspcdva ffnd eqidd wa 1onn a1i fnmptfvd mpbird )
+      ACBHIUBJZKFLZCMZIJZFHNZKZAVHGLZMZIJZFHNZKZVLGOHUCUDZCVMCJZVPVKVSVOVJFHVSV
+      NVIIVHVMCUEUAUFPAHQRZVQGVRNZDAHSRVTWAUGAHQDUHFHGSUITUJAHOCUKZCVRRACULRWBE
+      CUOTZOHCOHUMUNUPUQURUSAVGVKAHIIHFCHBAHOCWCUTVHBLZJIVAIHRZAVHHRVBVCVDWEAWD
+      HRVBVCVDVEPVF $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=