---

Step * of Lemma neg-bfs-append

∀[S:Type]. ∀[K:RngSig]. ∀[fs1,fs2:basic-formal-sum(K;S)].  (-(fs1 + fs2) = (-(fs1) + -(fs2)) ∈ basic-formal-sum(K;S))
BY
{ ((Auto THEN Unfold `neg-bfs` 0) THEN RWO "bag-map-append" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[fs1,fs2:basic-formal-sum(K;S)].    (-(fs1  +  fs2)  =  (-(fs1)  +  -(fs2)))


By

---

Latex:
((Auto  THEN  Unfold  `neg-bfs`  0)  THEN  RWO  "bag-map-append"  0  THEN  Auto)

---

Home Index