Step * 2 2 of Lemma fs-in-subtype-subspace


1. CRng
2. Type
3. Type
4. strong-subtype(T;S)
5. T ⊆S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a b ∈ T ∈ ℙ)
8. Point(free-vs(K;S))
9. Point(free-vs(K;S))
10. b1 basic-formal-sum(K;S)
11. b1 ∈ formal-sum(K;S)
12. bfs-predicate(K;S;p.snd(p) ∈ T;b1)
13. basic-formal-sum(K;S)
14. b ∈ formal-sum(K;S)
15. bfs-predicate(K;S;p.snd(p) ∈ T;b)
16. (b1 b) ∈ formal-sum(K;S)
⊢ bfs-predicate(K;S;p.snd(p) ∈ T;b1 b)
BY
(All (RepUR ``bfs-predicate``)
   THEN RepeatFor ((D THENA Auto))
   THEN BagMemberD (-1)
   THEN RepeatFor (D -1)
   THEN Auto) }


Latex:


Latex:

1.  K  :  CRng
2.  S  :  Type
3.  T  :  Type
4.  strong-subtype(T;S)
5.  T  \msubseteq{}r  S
6.  respects-equality(S;T)
7.  \mforall{}[a,b:S].    (a  =  b  \mmember{}  \mBbbP{})
8.  f  :  Point(free-vs(K;S))
9.  y  :  Point(free-vs(K;S))
10.  b1  :  basic-formal-sum(K;S)
11.  f  =  b1
12.  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b1)
13.  b  :  basic-formal-sum(K;S)
14.  y  =  b
15.  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b)
16.  f  +  y  =  (b1  +  b)
\mvdash{}  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b1  +  b)


By


Latex:
(All  (RepUR  ``bfs-predicate``)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  BagMemberD  (-1)
  THEN  RepeatFor  2  (D  -1)
  THEN  Auto)




Home Index