---

Step * 1 1 1 2 1 2 1 of Lemma respects-equality-bag


1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. f1 : ℕ||bs|| ⟶ ℕ||bs||
13. Inj(ℕ||bs||;ℕ||bs||;f1)
14. as = (bs o f1) ∈ (B List)
15. i : ℕ||bs||
16. j : ℕ||bs||
17. i = (f1 j) ∈ ℤ
⊢ bs[f1 j] ∈ B
BY
{ (StrengthenEquation (-4) THEN ApFunToHypEquands `Z' ⌜Z[j]⌝ ⌜B⌝ (-1)⋅) }

1
.....fun wf..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. f1 : ℕ||bs|| ⟶ ℕ||bs||
13. Inj(ℕ||bs||;ℕ||bs||;f1)
14. as = (bs o f1) ∈ (B List)
15. i : ℕ||bs||
16. j : ℕ||bs||
17. i = (f1 j) ∈ ℤ
18. as = (bs o f1) ∈ {z:B List| (z = as ∈ (B List)) ∧ (z = (bs o f1) ∈ (B List))} 
19. Z : {z:B List| (z = as ∈ (B List)) ∧ (z = (bs o f1) ∈ (B List))} 
⊢ Z[j] = Z[j] ∈ B

2
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. f1 : ℕ||bs|| ⟶ ℕ||bs||
13. Inj(ℕ||bs||;ℕ||bs||;f1)
14. as = (bs o f1) ∈ (B List)
15. i : ℕ||bs||
16. j : ℕ||bs||
17. i = (f1 j) ∈ ℤ
18. as = (bs o f1) ∈ {z:B List| (z = as ∈ (B List)) ∧ (z = (bs o f1) ∈ (B List))} 
19. as[j] = (bs o f1)[j] ∈ B
⊢ bs[f1 j] ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  respects-equality(A;B)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
7.  as  \mmember{}  B  List
8.  f  :  \mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||
9.  Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f)
10.  as  =  (bs  o  f)
11.  as  =  (bs  o  f)
12.  f1  :  \mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||
13.  Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f1)
14.  as  =  (bs  o  f1)
15.  i  :  \mBbbN{}||bs||
16.  j  :  \mBbbN{}||bs||
17.  i  =  (f1  j)
\mvdash{}  bs[f1  j]  \mmember{}  B


By

---

Latex:
(StrengthenEquation  (-4)  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z[j]\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}  (-1)\mcdot{})

---

Home Index