Step
*
of Lemma
orderedpair-fsts_functionality
∀a,b:coSet{i:l}.  (seteq(a;b) 
⇒ seteq(orderedpair-fsts(a);orderedpair-fsts(b)))
BY
{ Auto }
Latex:
Latex:
\mforall{}a,b:coSet\{i:l\}.    (seteq(a;b)  {}\mRightarrow{}  seteq(orderedpair-fsts(a);orderedpair-fsts(b)))
By
Latex:
Auto
Home
Index