Revert "[add] funcel1; [propose] funcel2"

This reverts commit 5fb5705.

Author: zwang123

set.mm

@@ -835491,33 +835491,6 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
           GHZCGHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
   $}
 
-  ${
-    funcel1.b $e |- B = ( Base ` D ) $.
-    funcel1.f $e |- ( ph -> F ( D Func E ) G ) $.
-    funcel1.x $e |- ( ph -> X e. B ) $.
-
-    ${
-    funcel1.c $e |- C = ( Base ` E ) $.
-    $( The object part of a functor maps into the base set.
-            (Contributed by Zhi Wang,
-       17-Sep-2025.) $)
-    funcel1 $p |- ( ph -> ( F ` X ) e. C ) $=
-    ( funcf1 ffvelcdmd ) ABCHFABCDEFGILJMKN $.
-    $}
-
-    ${
-    funcel2.h $e |- H = ( Hom ` D ) $.
-    funcel2.j $e |- J = ( Hom ` E ) $.
-    funcel2.y $e |- ( ph -> Y e. B ) $.
-    funcel2.m $e |- ( ph -> M e. ( X H Y ) ) $.
-    $( The morphism part of a functor maps into the hom set.
-            (Contributed by Zhi Wang,
-       17-Sep-2025.) $)
-    funcel2 $p |- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) ) $=
-    ( ) ? $.
-    $}
-  $}
-
   ${
     $d B x y z $.  $d F x y z $.  $d G x y z $.  $d H x y z $.  $d J x y z $.
     $( A utility theorem for proving equivalence of "is a functor".