---

Step * of Lemma fin_spr_mem_in_fin_spr

B: List  . f:fin_spr(B).  (f  fspr(B))
BY
{ Auto }

1
1. B :  List  @i
2. f : fin_spr(B)@i
 (f  fspr(B))


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:fin\_spr(B).    (f  \mmember{}  fspr(B))


By

Auto



Home Index