---

Step * of Lemma int_dot_cons_lemma

∀bs,b,as,a:Top.  ([a / as] ⋅ [b / bs] ~ (a * b) + as ⋅ bs)
BY
{ (UnivCD THENA Auto) }

1
1. bs : Top@i
2. b : Top@i
3. as : Top@i
4. a : Top@i
⊢ [a / as] ⋅ [b / bs] ~ (a * b) + as ⋅ bs

---

Latex:

---

Latex:
\mforall{}bs,b,as,a:Top.    ([a  /  as]  \mcdot{}  [b  /  bs]  \msim{}  (a  *  b)  +  as  \mcdot{}  bs)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index