---

Step * 1 1 1 of Lemma mod_times_mssum_r

.....set predicate..... 
1. s : DSet
2. r : Rng
3. m : algebra{i:l}(r)
4. f : |s| ⟶ m.car
5. u : m.car
6. a : MSet{s}
⊢ IsMonHom{m↓grp,m↓grp}(λy.(m.times y u))
BY
{ ((BLemma `grp_hom_formation` 
THENM Reduce 0 
THENM RepD) THENA Auto) }

1
1. s : DSet
2. r : Rng
3. m : algebra{i:l}(r)
4. f : |s| ⟶ m.car
5. u : m.car
6. a : MSet{s}
7. a1 : m.car
8. b : m.car
⊢ (m.times (a1 m.plus b) u) = ((m.times a1 u) m.plus (m.times b u)) ∈ m.car

---

Latex:

---

Latex:
.....set  predicate..... 
1.  s  :  DSet
2.  r  :  Rng
3.  m  :  algebra\{i:l\}(r)
4.  f  :  |s|  {}\mrightarrow{}  m.car
5.  u  :  m.car
6.  a  :  MSet\{s\}
\mvdash{}  IsMonHom\{m\mdownarrow{}grp,m\mdownarrow{}grp\}(\mlambda{}y.(m.times  y  u))


By

---

Latex:
((BLemma  `grp\_hom\_formation` 
THENM  Reduce  0 
THENM  RepD)  THENA  Auto)

---

Home Index