---

Step * of Lemma non-zero-vector-implies

∀r:RngSig
  ((∀x,y:|r|.  Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. ∀a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} .  (∃i:ℕk [(¬((a i) = 0 ∈ |r|))])))
BY
{ (Auto
   THEN ((Assert ∃i:ℕk. (¬((a i) = 0 ∈ |r|)) BY
                (SupposeNot
                 THEN Assert ⌜False⌝⋅
                 THEN Auto
                 THEN RepeatFor 2 (D -2)
                 THEN (FunExt THENA Auto)
                 THEN RepUR ``zero-vector`` 0
                 THEN SupposeNot
                 THEN D -3
                 THEN Auto))
        THENM ParallelLast
        )
   ) }

---

Latex:

---

Latex:
\mforall{}r:RngSig
    ((\mforall{}x,y:|r|.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mforall{}a:\{a:\mBbbN{}k  {}\mrightarrow{}  |r||  \mneg{}(a  =  0)\}  .    (\mexists{}i:\mBbbN{}k  [(\mneg{}((a  i)  =  0))])))


By

---

Latex:
(Auto
  THEN  ((Assert  \mexists{}i:\mBbbN{}k.  (\mneg{}((a  i)  =  0))  BY
                            (SupposeNot
                              THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                              THEN  Auto
                              THEN  RepeatFor  2  (D  -2)
                              THEN  (FunExt  THENA  Auto)
                              THEN  RepUR  ``zero-vector``  0
                              THEN  SupposeNot
                              THEN  D  -3
                              THEN  Auto))
            THENM  ParallelLast
            )
  )

---

Home Index