Theorem mulscom

Description: Surreal multiplication commutes. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Assertion	mulscom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B=B{\cdot }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) : No typesetting found for |- ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) with typecode |-
2		oveq2	Could not format ( x = xO -> ( y x.s x ) = ( y x.s xO ) ) : No typesetting found for |- ( x = xO -> ( y x.s x ) = ( y x.s xO ) ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = xO -> ( ( x x.s y ) = ( y x.s x ) <-> ( xO x.s y ) = ( y x.s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s y ) = ( y x.s x ) <-> ( xO x.s y ) = ( y x.s xO ) ) ) with typecode |-
4		oveq2	Could not format ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) : No typesetting found for |- ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) with typecode |-
5		oveq1	Could not format ( y = yO -> ( y x.s xO ) = ( yO x.s xO ) ) : No typesetting found for |- ( y = yO -> ( y x.s xO ) = ( yO x.s xO ) ) with typecode |-
6	4 5	eqeq12d	Could not format ( y = yO -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) with typecode |-
7		oveq1	Could not format ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) : No typesetting found for |- ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) with typecode |-
8		oveq2	Could not format ( x = xO -> ( yO x.s x ) = ( yO x.s xO ) ) : No typesetting found for |- ( x = xO -> ( yO x.s x ) = ( yO x.s xO ) ) with typecode |-
9	7 8	eqeq12d	Could not format ( x = xO -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( xO x.s yO ) = ( yO x.s xO ) ) ) with typecode |-
10		oveq1	$$⊢x=A\to x{\cdot }_{s}y=A{\cdot }_{s}y$$
11		oveq2	$$⊢x=A\to y{\cdot }_{s}x=y{\cdot }_{s}A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(x{\cdot }_{s}y=y{\cdot }_{s}x\leftrightarrow A{\cdot }_{s}y=y{\cdot }_{s}A\right)$$
13		oveq2	$$⊢y=B\to A{\cdot }_{s}y=A{\cdot }_{s}B$$
14		oveq1	$$⊢y=B\to y{\cdot }_{s}A=B{\cdot }_{s}A$$
15	13 14	eqeq12d	$$⊢y=B\to \left(A{\cdot }_{s}y=y{\cdot }_{s}A\leftrightarrow A{\cdot }_{s}B=B{\cdot }_{s}A\right)$$
16		oveq1	Could not format ( xO = p -> ( xO x.s y ) = ( p x.s y ) ) : No typesetting found for |- ( xO = p -> ( xO x.s y ) = ( p x.s y ) ) with typecode |-
17		oveq2	Could not format ( xO = p -> ( y x.s xO ) = ( y x.s p ) ) : No typesetting found for |- ( xO = p -> ( y x.s xO ) = ( y x.s p ) ) with typecode |-
18	16 17	eqeq12d	Could not format ( xO = p -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( p x.s y ) = ( y x.s p ) ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( p x.s y ) = ( y x.s p ) ) ) with typecode |-
19		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
20		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( _Left ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( _Left ` x ) ) with typecode |-
21		elun1	$$⊢p\in L\left(x\right)\to p\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
22	20 21	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
23	18 19 22	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s y ) = ( y x.s p ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s y ) = ( y x.s p ) ) with typecode |-
24		oveq2	Could not format ( yO = q -> ( x x.s yO ) = ( x x.s q ) ) : No typesetting found for |- ( yO = q -> ( x x.s yO ) = ( x x.s q ) ) with typecode |-
25		oveq1	Could not format ( yO = q -> ( yO x.s x ) = ( q x.s x ) ) : No typesetting found for |- ( yO = q -> ( yO x.s x ) = ( q x.s x ) ) with typecode |-
26	24 25	eqeq12d	Could not format ( yO = q -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s q ) = ( q x.s x ) ) ) : No typesetting found for |- ( yO = q -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s q ) = ( q x.s x ) ) ) with typecode |-
27		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
28		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( _Left ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( _Left ` y ) ) with typecode |-
29		elun1	$$⊢q\in L\left(y\right)\to q\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
30	28 29	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
31	26 27 30	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( x x.s q ) = ( q x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( x x.s q ) = ( q x.s x ) ) with typecode |-
32	23 31	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( y x.s p ) +s ( q x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( y x.s p ) +s ( q x.s x ) ) ) with typecode |-
33		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> y e. No ) with typecode |-
34		leftssno	$$⊢L\left(x\right)\subseteq \mathrm{No}$$
35	34 20	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> p e. No ) with typecode |-
36	33 35	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( y x.s p ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( y x.s p ) e. No ) with typecode |-
37		leftssno	$$⊢L\left(y\right)\subseteq \mathrm{No}$$
38	37 28	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> q e. No ) with typecode |-
39		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> x e. No ) with typecode |-
40	38 39	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( q x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( q x.s x ) e. No ) with typecode |-
41	36 40	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( y x.s p ) +s ( q x.s x ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( y x.s p ) +s ( q x.s x ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) with typecode |-
42	32 41	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( p x.s y ) +s ( x x.s q ) ) = ( ( q x.s x ) +s ( y x.s p ) ) ) with typecode |-
43		oveq1	Could not format ( xO = p -> ( xO x.s yO ) = ( p x.s yO ) ) : No typesetting found for |- ( xO = p -> ( xO x.s yO ) = ( p x.s yO ) ) with typecode |-
44		oveq2	Could not format ( xO = p -> ( yO x.s xO ) = ( yO x.s p ) ) : No typesetting found for |- ( xO = p -> ( yO x.s xO ) = ( yO x.s p ) ) with typecode |-
45	43 44	eqeq12d	Could not format ( xO = p -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( p x.s yO ) = ( yO x.s p ) ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( p x.s yO ) = ( yO x.s p ) ) ) with typecode |-
46		oveq2	Could not format ( yO = q -> ( p x.s yO ) = ( p x.s q ) ) : No typesetting found for |- ( yO = q -> ( p x.s yO ) = ( p x.s q ) ) with typecode |-
47		oveq1	Could not format ( yO = q -> ( yO x.s p ) = ( q x.s p ) ) : No typesetting found for |- ( yO = q -> ( yO x.s p ) = ( q x.s p ) ) with typecode |-
48	46 47	eqeq12d	Could not format ( yO = q -> ( ( p x.s yO ) = ( yO x.s p ) <-> ( p x.s q ) = ( q x.s p ) ) ) : No typesetting found for |- ( yO = q -> ( ( p x.s yO ) = ( yO x.s p ) <-> ( p x.s q ) = ( q x.s p ) ) ) with typecode |-
49		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
50	45 48 49 22 30	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s q ) = ( q x.s p ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( p x.s q ) = ( q x.s p ) ) with typecode |-
51	42 50	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) with typecode |-
52	51	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( p e. ( _Left ` x ) /\ q e. ( _Left ` y ) ) ) -> ( a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
53	52	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
54		rexcom	$$⊢\exists p\in L\left(x\right)\exists q\in L\left(y\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\leftrightarrow \exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)$$
55	53 54	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) ) ) with typecode |-
56	55	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } ) with typecode |-
57		oveq1	Could not format ( xO = r -> ( xO x.s y ) = ( r x.s y ) ) : No typesetting found for |- ( xO = r -> ( xO x.s y ) = ( r x.s y ) ) with typecode |-
58		oveq2	Could not format ( xO = r -> ( y x.s xO ) = ( y x.s r ) ) : No typesetting found for |- ( xO = r -> ( y x.s xO ) = ( y x.s r ) ) with typecode |-
59	57 58	eqeq12d	Could not format ( xO = r -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( r x.s y ) = ( y x.s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( r x.s y ) = ( y x.s r ) ) ) with typecode |-
60		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
61		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( _Right ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( _Right ` x ) ) with typecode |-
62		elun2	$$⊢r\in R\left(x\right)\to r\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
63	61 62	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
64	59 60 63	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s y ) = ( y x.s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s y ) = ( y x.s r ) ) with typecode |-
65		oveq2	Could not format ( yO = s -> ( x x.s yO ) = ( x x.s s ) ) : No typesetting found for |- ( yO = s -> ( x x.s yO ) = ( x x.s s ) ) with typecode |-
66		oveq1	Could not format ( yO = s -> ( yO x.s x ) = ( s x.s x ) ) : No typesetting found for |- ( yO = s -> ( yO x.s x ) = ( s x.s x ) ) with typecode |-
67	65 66	eqeq12d	Could not format ( yO = s -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s s ) = ( s x.s x ) ) ) : No typesetting found for |- ( yO = s -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s s ) = ( s x.s x ) ) ) with typecode |-
68		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
69		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( _Right ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( _Right ` y ) ) with typecode |-
70		elun2	$$⊢s\in R\left(y\right)\to s\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
71	69 70	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
72	67 68 71	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( x x.s s ) = ( s x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( x x.s s ) = ( s x.s x ) ) with typecode |-
73	64 72	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( y x.s r ) +s ( s x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( y x.s r ) +s ( s x.s x ) ) ) with typecode |-
74		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> y e. No ) with typecode |-
75		rightssno	$$⊢R\left(x\right)\subseteq \mathrm{No}$$
76	75 61	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> r e. No ) with typecode |-
77	74 76	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( y x.s r ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( y x.s r ) e. No ) with typecode |-
78		rightssno	$$⊢R\left(y\right)\subseteq \mathrm{No}$$
79	78 69	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> s e. No ) with typecode |-
80		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> x e. No ) with typecode |-
81	79 80	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( s x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( s x.s x ) e. No ) with typecode |-
82	77 81	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( y x.s r ) +s ( s x.s x ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( y x.s r ) +s ( s x.s x ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) with typecode |-
83	73 82	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( r x.s y ) +s ( x x.s s ) ) = ( ( s x.s x ) +s ( y x.s r ) ) ) with typecode |-
84		oveq1	Could not format ( xO = r -> ( xO x.s yO ) = ( r x.s yO ) ) : No typesetting found for |- ( xO = r -> ( xO x.s yO ) = ( r x.s yO ) ) with typecode |-
85		oveq2	Could not format ( xO = r -> ( yO x.s xO ) = ( yO x.s r ) ) : No typesetting found for |- ( xO = r -> ( yO x.s xO ) = ( yO x.s r ) ) with typecode |-
86	84 85	eqeq12d	Could not format ( xO = r -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( r x.s yO ) = ( yO x.s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( r x.s yO ) = ( yO x.s r ) ) ) with typecode |-
87		oveq2	Could not format ( yO = s -> ( r x.s yO ) = ( r x.s s ) ) : No typesetting found for |- ( yO = s -> ( r x.s yO ) = ( r x.s s ) ) with typecode |-
88		oveq1	Could not format ( yO = s -> ( yO x.s r ) = ( s x.s r ) ) : No typesetting found for |- ( yO = s -> ( yO x.s r ) = ( s x.s r ) ) with typecode |-
89	87 88	eqeq12d	Could not format ( yO = s -> ( ( r x.s yO ) = ( yO x.s r ) <-> ( r x.s s ) = ( s x.s r ) ) ) : No typesetting found for |- ( yO = s -> ( ( r x.s yO ) = ( yO x.s r ) <-> ( r x.s s ) = ( s x.s r ) ) ) with typecode |-
90		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
91	86 89 90 63 71	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s s ) = ( s x.s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( r x.s s ) = ( s x.s r ) ) with typecode |-
92	83 91	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) with typecode |-
93	92	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( r e. ( _Right ` x ) /\ s e. ( _Right ` y ) ) ) -> ( b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
94	93	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
95		rexcom	$$⊢\exists r\in R\left(x\right)\exists s\in R\left(y\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\leftrightarrow \exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)$$
96	94 95	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) ) ) with typecode |-
97	96	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) with typecode |-
98	56 97	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) ) with typecode |-
99		oveq1	Could not format ( xO = t -> ( xO x.s y ) = ( t x.s y ) ) : No typesetting found for |- ( xO = t -> ( xO x.s y ) = ( t x.s y ) ) with typecode |-
100		oveq2	Could not format ( xO = t -> ( y x.s xO ) = ( y x.s t ) ) : No typesetting found for |- ( xO = t -> ( y x.s xO ) = ( y x.s t ) ) with typecode |-
101	99 100	eqeq12d	Could not format ( xO = t -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( t x.s y ) = ( y x.s t ) ) ) : No typesetting found for |- ( xO = t -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( t x.s y ) = ( y x.s t ) ) ) with typecode |-
102		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
103		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( _Left ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( _Left ` x ) ) with typecode |-
104		elun1	$$⊢t\in L\left(x\right)\to t\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
105	103 104	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
106	101 102 105	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s y ) = ( y x.s t ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s y ) = ( y x.s t ) ) with typecode |-
107		oveq2	Could not format ( yO = u -> ( x x.s yO ) = ( x x.s u ) ) : No typesetting found for |- ( yO = u -> ( x x.s yO ) = ( x x.s u ) ) with typecode |-
108		oveq1	Could not format ( yO = u -> ( yO x.s x ) = ( u x.s x ) ) : No typesetting found for |- ( yO = u -> ( yO x.s x ) = ( u x.s x ) ) with typecode |-
109	107 108	eqeq12d	Could not format ( yO = u -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s u ) = ( u x.s x ) ) ) : No typesetting found for |- ( yO = u -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s u ) = ( u x.s x ) ) ) with typecode |-
110		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
111		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( _Right ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( _Right ` y ) ) with typecode |-
112		elun2	$$⊢u\in R\left(y\right)\to u\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
113	111 112	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
114	109 110 113	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( x x.s u ) = ( u x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( x x.s u ) = ( u x.s x ) ) with typecode |-
115	106 114	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( y x.s t ) +s ( u x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( y x.s t ) +s ( u x.s x ) ) ) with typecode |-
116		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> y e. No ) with typecode |-
117	34 103	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> t e. No ) with typecode |-
118	116 117	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( y x.s t ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( y x.s t ) e. No ) with typecode |-
119	78 111	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> u e. No ) with typecode |-
120		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> x e. No ) with typecode |-
121	119 120	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( u x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( u x.s x ) e. No ) with typecode |-
122	118 121	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( y x.s t ) +s ( u x.s x ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( y x.s t ) +s ( u x.s x ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) with typecode |-
123	115 122	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( t x.s y ) +s ( x x.s u ) ) = ( ( u x.s x ) +s ( y x.s t ) ) ) with typecode |-
124		oveq1	Could not format ( xO = t -> ( xO x.s yO ) = ( t x.s yO ) ) : No typesetting found for |- ( xO = t -> ( xO x.s yO ) = ( t x.s yO ) ) with typecode |-
125		oveq2	Could not format ( xO = t -> ( yO x.s xO ) = ( yO x.s t ) ) : No typesetting found for |- ( xO = t -> ( yO x.s xO ) = ( yO x.s t ) ) with typecode |-
126	124 125	eqeq12d	Could not format ( xO = t -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( t x.s yO ) = ( yO x.s t ) ) ) : No typesetting found for |- ( xO = t -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( t x.s yO ) = ( yO x.s t ) ) ) with typecode |-
127		oveq2	Could not format ( yO = u -> ( t x.s yO ) = ( t x.s u ) ) : No typesetting found for |- ( yO = u -> ( t x.s yO ) = ( t x.s u ) ) with typecode |-
128		oveq1	Could not format ( yO = u -> ( yO x.s t ) = ( u x.s t ) ) : No typesetting found for |- ( yO = u -> ( yO x.s t ) = ( u x.s t ) ) with typecode |-
129	127 128	eqeq12d	Could not format ( yO = u -> ( ( t x.s yO ) = ( yO x.s t ) <-> ( t x.s u ) = ( u x.s t ) ) ) : No typesetting found for |- ( yO = u -> ( ( t x.s yO ) = ( yO x.s t ) <-> ( t x.s u ) = ( u x.s t ) ) ) with typecode |-
130		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
131	126 129 130 105 113	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s u ) = ( u x.s t ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( t x.s u ) = ( u x.s t ) ) with typecode |-
132	123 131	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) with typecode |-
133	132	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( t e. ( _Left ` x ) /\ u e. ( _Right ` y ) ) ) -> ( c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
134	133	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
135		rexcom	$$⊢\exists t\in L\left(x\right)\exists u\in R\left(y\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\leftrightarrow \exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)$$
136	134 135	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) ) ) with typecode |-
137	136	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) with typecode |-
138		oveq1	Could not format ( xO = v -> ( xO x.s y ) = ( v x.s y ) ) : No typesetting found for |- ( xO = v -> ( xO x.s y ) = ( v x.s y ) ) with typecode |-
139		oveq2	Could not format ( xO = v -> ( y x.s xO ) = ( y x.s v ) ) : No typesetting found for |- ( xO = v -> ( y x.s xO ) = ( y x.s v ) ) with typecode |-
140	138 139	eqeq12d	Could not format ( xO = v -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( v x.s y ) = ( y x.s v ) ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s y ) = ( y x.s xO ) <-> ( v x.s y ) = ( y x.s v ) ) ) with typecode |-
141		simplr2	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) ) with typecode |-
142		simprl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( _Right ` x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( _Right ` x ) ) with typecode |-
143		elun2	$$⊢v\in R\left(x\right)\to v\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
144	142 143	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
145	140 141 144	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s y ) = ( y x.s v ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s y ) = ( y x.s v ) ) with typecode |-
146		oveq2	Could not format ( yO = w -> ( x x.s yO ) = ( x x.s w ) ) : No typesetting found for |- ( yO = w -> ( x x.s yO ) = ( x x.s w ) ) with typecode |-
147		oveq1	Could not format ( yO = w -> ( yO x.s x ) = ( w x.s x ) ) : No typesetting found for |- ( yO = w -> ( yO x.s x ) = ( w x.s x ) ) with typecode |-
148	146 147	eqeq12d	Could not format ( yO = w -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s w ) = ( w x.s x ) ) ) : No typesetting found for |- ( yO = w -> ( ( x x.s yO ) = ( yO x.s x ) <-> ( x x.s w ) = ( w x.s x ) ) ) with typecode |-
149		simplr3	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) with typecode |-
150		simprr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( _Left ` y ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( _Left ` y ) ) with typecode |-
151		elun1	$$⊢w\in L\left(y\right)\to w\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
152	150 151	syl	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
153	148 149 152	rspcdva	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( x x.s w ) = ( w x.s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( x x.s w ) = ( w x.s x ) ) with typecode |-
154	145 153	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( y x.s v ) +s ( w x.s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( y x.s v ) +s ( w x.s x ) ) ) with typecode |-
155		simpllr	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> y e. No ) with typecode |-
156	75 142	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> v e. No ) with typecode |-
157	155 156	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( y x.s v ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( y x.s v ) e. No ) with typecode |-
158	37 150	sselid	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> w e. No ) with typecode |-
159		simplll	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> x e. No ) with typecode |-
160	158 159	mulscld	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( w x.s x ) e. No ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( w x.s x ) e. No ) with typecode |-
161	157 160	addscomd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( y x.s v ) +s ( w x.s x ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( y x.s v ) +s ( w x.s x ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) with typecode |-
162	154 161	eqtrd	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( v x.s y ) +s ( x x.s w ) ) = ( ( w x.s x ) +s ( y x.s v ) ) ) with typecode |-
163		oveq1	Could not format ( xO = v -> ( xO x.s yO ) = ( v x.s yO ) ) : No typesetting found for |- ( xO = v -> ( xO x.s yO ) = ( v x.s yO ) ) with typecode |-
164		oveq2	Could not format ( xO = v -> ( yO x.s xO ) = ( yO x.s v ) ) : No typesetting found for |- ( xO = v -> ( yO x.s xO ) = ( yO x.s v ) ) with typecode |-
165	163 164	eqeq12d	Could not format ( xO = v -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( v x.s yO ) = ( yO x.s v ) ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s yO ) = ( yO x.s xO ) <-> ( v x.s yO ) = ( yO x.s v ) ) ) with typecode |-
166		oveq2	Could not format ( yO = w -> ( v x.s yO ) = ( v x.s w ) ) : No typesetting found for |- ( yO = w -> ( v x.s yO ) = ( v x.s w ) ) with typecode |-
167		oveq1	Could not format ( yO = w -> ( yO x.s v ) = ( w x.s v ) ) : No typesetting found for |- ( yO = w -> ( yO x.s v ) = ( w x.s v ) ) with typecode |-
168	166 167	eqeq12d	Could not format ( yO = w -> ( ( v x.s yO ) = ( yO x.s v ) <-> ( v x.s w ) = ( w x.s v ) ) ) : No typesetting found for |- ( yO = w -> ( ( v x.s yO ) = ( yO x.s v ) <-> ( v x.s w ) = ( w x.s v ) ) ) with typecode |-
169		simplr1	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) ) with typecode |-
170	165 168 169 144 152	rspc2dv	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s w ) = ( w x.s v ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( v x.s w ) = ( w x.s v ) ) with typecode |-
171	162 170	oveq12d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) with typecode |-
172	171	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) /\ ( v e. ( _Right ` x ) /\ w e. ( _Left ` y ) ) ) -> ( d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
173	172	2rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
174		rexcom	$$⊢\exists v\in R\left(x\right)\exists w\in L\left(y\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\leftrightarrow \exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)$$
175	173 174	bitrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) ) ) with typecode |-
176	175	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) with typecode |-
177	137 176	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } u. { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } u. { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } ) ) with typecode |-
178		uncom	$$⊢\left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\cup \left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}=\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}$$
179	177 178	eqtrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) with typecode |-
180	98 179	oveq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) with typecode |-
181		mulsval	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to x{\cdot }_{s}y=\left(\left\{a|\exists p\in L\left(x\right)\exists q\in L\left(y\right)a=\left(\left(p{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(x\right)\exists s\in R\left(y\right)b=\left(\left(r{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(x\right)\exists u\in R\left(y\right)c=\left(\left(t{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(x\right)\exists w\in L\left(y\right)d=\left(\left(v{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
182	181	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p x.s y ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r x.s y ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t x.s y ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v x.s y ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
183		mulsval	$$⊢\left(y\in \mathrm{No}\wedge x\in \mathrm{No}\right)\to y{\cdot }_{s}x=\left(\left\{a|\exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\right\}\cup \left\{b|\exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\right\}\right){|}_s\left(\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\right)$$
184	183	ancoms	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to y{\cdot }_{s}x=\left(\left\{a|\exists q\in L\left(y\right)\exists p\in L\left(x\right)a=\left(\left(q{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}p\right)\right){-}_s\left(q{\cdot }_{s}p\right)\right\}\cup \left\{b|\exists s\in R\left(y\right)\exists r\in R\left(x\right)b=\left(\left(s{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}r\right)\right){-}_s\left(s{\cdot }_{s}r\right)\right\}\right){|}_s\left(\left\{d|\exists w\in L\left(y\right)\exists v\in R\left(x\right)d=\left(\left(w{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}v\right)\right){-}_s\left(w{\cdot }_{s}v\right)\right\}\cup \left\{c|\exists u\in R\left(y\right)\exists t\in L\left(x\right)c=\left(\left(u{\cdot }_{s}x\right){+}_s\left(y{\cdot }_{s}t\right)\right){-}_s\left(u{\cdot }_{s}t\right)\right\}\right)$$
185	184	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( y x.s x ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( y x.s x ) = ( ( { a | E. q e. ( _Left ` y ) E. p e. ( _Left ` x ) a = ( ( ( q x.s x ) +s ( y x.s p ) ) -s ( q x.s p ) ) } u. { b | E. s e. ( _Right ` y ) E. r e. ( _Right ` x ) b = ( ( ( s x.s x ) +s ( y x.s r ) ) -s ( s x.s r ) ) } ) |s ( { d | E. w e. ( _Left ` y ) E. v e. ( _Right ` x ) d = ( ( ( w x.s x ) +s ( y x.s v ) ) -s ( w x.s v ) ) } u. { c | E. u e. ( _Right ` y ) E. t e. ( _Left ` x ) c = ( ( ( u x.s x ) +s ( y x.s t ) ) -s ( u x.s t ) ) } ) ) ) with typecode |-
186	180 182 185	3eqtr4d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( y x.s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) ) -> ( x x.s y ) = ( y x.s x ) ) with typecode |-
187	186	ex	Could not format ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) -> ( x x.s y ) = ( y x.s x ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s yO ) = ( yO x.s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s y ) = ( y x.s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s yO ) = ( yO x.s x ) ) -> ( x x.s y ) = ( y x.s x ) ) ) with typecode |-
188	3 6 9 12 15 187	no2inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B=B{\cdot }_{s}A$$