GCD_1

:: GCD_1 semantic presentation

K99() is V140() V141() V142() V143() V144() V145() V146() Element of K19(K95())
K95() is V140() V141() V142() V146() set
K19(K95()) is non empty set
K96() is V140() V146() set
K97() is V140() V141() V142() V143() V146() set
K98() is V140() V141() V142() V143() V144() V146() set
K20(K96(),K96()) is set
K19(K20(K96(),K96())) is non empty set
K20(K20(K96(),K96()),K96()) is set
K19(K20(K20(K96(),K96()),K96())) is non empty set
K20(K95(),K95()) is set
K19(K20(K95(),K95())) is non empty set
K20(K20(K95(),K95()),K95()) is set
K19(K20(K20(K95(),K95()),K95())) is non empty set
K20(K97(),K97()) is set
K19(K20(K97(),K97())) is non empty set
K20(K20(K97(),K97()),K97()) is set
K19(K20(K20(K97(),K97()),K97())) is non empty set
K20(K98(),K98()) is set
K19(K20(K98(),K98())) is non empty set
K20(K20(K98(),K98()),K98()) is set
K19(K20(K20(K98(),K98()),K98())) is non empty set
K20(K99(),K99()) is set
K20(K20(K99(),K99()),K99()) is set
K19(K20(K20(K99(),K99()),K99())) is non empty set
K94() is V140() V141() V142() V143() V144() V145() V146() set
K19(K94()) is non empty set
K19(K99()) is non empty set
K339() is non empty strict multMagma
the carrier of K339() is non empty set
K344() is non empty strict unital Group-like associative commutative V162() V163() V164() V165() V166() V167() multMagma
K345() is non empty strict associative commutative V165() V166() V167() M13(K344())
K346() is non empty strict unital associative commutative V165() V166() V167() V168() M16(K344(),K345())
K348() is non empty strict unital associative commutative multMagma
K349() is non empty strict unital associative commutative V168() M13(K348())
{} is empty V140() V141() V142() V143() V144() V145() V146() set
the empty V140() V141() V142() V143() V144() V145() V146() set is empty V140() V141() V142() V143() V144() V145() V146() set
1 is non empty set
0 is empty V21() V28() V29() V30() V31() V127() V140() V141() V142() V143() V144() V145() V146() Element of K99()
F is non empty multLoopStr
the carrier of F is non empty set
1. F is Element of the carrier of F
a is Element of the carrier of F
(1. F) * a is Element of the carrier of F
a * (1. F) is Element of the carrier of F
F is non empty doubleLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
b + r2 is Element of the carrier of F
a * (b + r2) is Element of the carrier of F
a * b is Element of the carrier of F
a * r2 is Element of the carrier of F
(a * b) + (a * r2) is Element of the carrier of F
(b + r2) * a is Element of the carrier of F
b * a is Element of the carrier of F
r2 * a is Element of the carrier of F
(b * a) + (r2 * a) is Element of the carrier of F
(b * a) + (a * r2) is Element of the carrier of F
F is non empty doubleLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
b + r2 is Element of the carrier of F
a * (b + r2) is Element of the carrier of F
a * b is Element of the carrier of F
a * r2 is Element of the carrier of F
(a * b) + (a * r2) is Element of the carrier of F
(b + r2) * a is Element of the carrier of F
b * a is Element of the carrier of F
r2 * a is Element of the carrier of F
(b * a) + (r2 * a) is Element of the carrier of F
(a * b) + (r2 * a) is Element of the carrier of F
F is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
F_Real is non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
K143() is V6() V18(K20(K95(),K95()),K95()) Element of K19(K20(K20(K95(),K95()),K95()))
K145() is V6() V18(K20(K95(),K95()),K95()) Element of K19(K20(K20(K95(),K95()),K95()))
doubleLoopStr(# K95(),K143(),K145(),1,0 #) is strict doubleLoopStr
the carrier of F_Real is non empty V12() V140() V141() V142() set
0. F_Real is V21() V29() V48( F_Real ) V127() Element of the carrier of F_Real
a is V21() V29() V127() Element of the carrier of F_Real
b is V21() V29() V127() Element of the carrier of F_Real
a * b is V21() V29() V127() Element of the carrier of F_Real
K121(a,b) is V21() V29() V127() Element of K95()
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a * b is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
b * a is Element of the carrier of F
r2 * a is Element of the carrier of F
- (a * r2) is Element of the carrier of F
(a * b) + (- (a * r2)) is Element of the carrier of F
- r2 is Element of the carrier of F
a * (- r2) is Element of the carrier of F
(a * b) + (a * (- r2)) is Element of the carrier of F
b + (- r2) is Element of the carrier of F
a * (b + (- r2)) is Element of the carrier of F
b - r2 is Element of the carrier of F
a * (b - r2) is Element of the carrier of F
(b - r2) + r2 is Element of the carrier of F
(b + (- r2)) + r2 is Element of the carrier of F
r2 + (- r2) is Element of the carrier of F
b + (r2 + (- r2)) is Element of the carrier of F
b + (0. F) is Element of the carrier of F
F is non empty multMagma
the carrier of F is non empty set
F is non empty right_unital multLoopStr
the carrier of F is non empty set
r2 is Element of the carrier of F
1. F is Element of the carrier of F
r2 * (1. F) is Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
F is non empty multLoopStr
the carrier of F is non empty set
r2 is Element of the carrier of F
s1 is Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
F is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
r2 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
b is Element of the carrier of F
a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
b * r2 is Element of the carrier of F
r2 is Element of the carrier of F
r2 * b is Element of the carrier of F
s1 is Element of the carrier of F
s1 * b is Element of the carrier of F
F is non empty associative multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
a * s1 is Element of the carrier of F
s2 is Element of the carrier of F
b * s2 is Element of the carrier of F
s1 * s2 is Element of the carrier of F
a * (s1 * s2) is Element of the carrier of F
F is non empty associative commutative multLoopStr
the carrier of F is non empty set
b is Element of the carrier of F
a is Element of the carrier of F
s1 is Element of the carrier of F
r2 is Element of the carrier of F
b * s1 is Element of the carrier of F
a * r2 is Element of the carrier of F
s2 is Element of the carrier of F
b * s2 is Element of the carrier of F
z2 is Element of the carrier of F
s1 * z2 is Element of the carrier of F
z2 * s2 is Element of the carrier of F
(b * s1) * (z2 * s2) is Element of the carrier of F
(b * s1) * z2 is Element of the carrier of F
((b * s1) * z2) * s2 is Element of the carrier of F
b * r2 is Element of the carrier of F
(b * r2) * s2 is Element of the carrier of F
F is non empty associative multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
F is non empty associative multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
r2 * a is Element of the carrier of F
r2 * b is Element of the carrier of F
s1 is Element of the carrier of F
a * s1 is Element of the carrier of F
(r2 * a) * s1 is Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
a * b is Element of the carrier of F
b * a is Element of the carrier of F
F is non empty associative multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
b * r2 is Element of the carrier of F
s1 is Element of the carrier of F
a * s1 is Element of the carrier of F
s1 * r2 is Element of the carrier of F
a * (s1 * r2) is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
a is Element of the carrier of F
(F,a,b) is Element of the carrier of F
(0. F) * b is Element of the carrier of F
(F,a,b) * b is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
1. F is Element of the carrier of F
a is Element of the carrier of F
(F,a,a) is Element of the carrier of F
(F,a,a) * a is Element of the carrier of F
(1. F) * a is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
(F,a,(1. F)) is Element of the carrier of F
(1. F) * a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,(1. F)) * (1. F) is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a * b is Element of the carrier of F
(F,(a * b),r2) is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
(F,a,r2) * b is Element of the carrier of F
(F,b,r2) is Element of the carrier of F
a * (F,b,r2) is Element of the carrier of F
(F,(a * b),r2) * r2 is Element of the carrier of F
(F,b,r2) * r2 is Element of the carrier of F
(a * (F,b,r2)) * r2 is Element of the carrier of F
(F,a,r2) * r2 is Element of the carrier of F
((F,a,r2) * b) * r2 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a + b is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
(F,b,r2) is Element of the carrier of F
(F,a,r2) + (F,b,r2) is Element of the carrier of F
(F,(a + b),r2) is Element of the carrier of F
(F,a,r2) * r2 is Element of the carrier of F
(F,b,r2) * r2 is Element of the carrier of F
((F,a,r2) + (F,b,r2)) * r2 is Element of the carrier of F
(F,r2,r2) is Element of the carrier of F
((F,a,r2) + (F,b,r2)) * (F,r2,r2) is Element of the carrier of F
1. F is Element of the carrier of F
((F,a,r2) + (F,b,r2)) * (1. F) is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
(F,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
s1 * r2 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
s1 is Element of the carrier of F
a is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b) is Element of the carrier of F
(F,r2,s1) is Element of the carrier of F
(F,a,b) * (F,r2,s1) is Element of the carrier of F
a * r2 is Element of the carrier of F
b * s1 is Element of the carrier of F
(F,(a * r2),(b * s1)) is Element of the carrier of F
(F,a,b) * b is Element of the carrier of F
(F,r2,s1) * s1 is Element of the carrier of F
(F,(a * r2),(b * s1)) * (b * s1) is Element of the carrier of F
((F,a,b) * b) * ((F,r2,s1) * s1) is Element of the carrier of F
b * ((F,r2,s1) * s1) is Element of the carrier of F
(F,a,b) * (b * ((F,r2,s1) * s1)) is Element of the carrier of F
(F,r2,s1) * (b * s1) is Element of the carrier of F
(F,a,b) * ((F,r2,s1) * (b * s1)) is Element of the carrier of F
((F,a,b) * (F,r2,s1)) * (b * s1) is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a * b is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
s1 is Element of the carrier of F
(a * b) * s1 is Element of the carrier of F
(F,(a * r2),a) is Element of the carrier of F
(F,a,a) is Element of the carrier of F
(F,a,a) * r2 is Element of the carrier of F
b * s1 is Element of the carrier of F
a * (b * s1) is Element of the carrier of F
(F,(a * (b * s1)),a) is Element of the carrier of F
(F,a,a) * (b * s1) is Element of the carrier of F
1. F is Element of the carrier of F
(1. F) * (b * s1) is Element of the carrier of F
(1. F) * r2 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
(0. F) * b is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
1. F is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a * b is Element of the carrier of F
(F,a,a) is Element of the carrier of F
(F,(a * b),a) is Element of the carrier of F
(F,a,a) * b is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
s1 is Element of the carrier of F
b * s1 is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
r2 * s1 is Element of the carrier of F
a * (r2 * s1) is Element of the carrier of F
1. F is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
1. F is Element of the carrier of F
a * (1. F) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
s2 is Element of the carrier of F
a * s2 is Element of the carrier of F
z2 is Element of the carrier of F
a * z2 is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
1. F is Element of the carrier of F
s1 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
a * (r2 * s1) is Element of the carrier of F
b * s1 is Element of the carrier of F
s2 is Element of the carrier of F
a * s2 is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
r2 is Element of the carrier of F
a * r2 is Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
s2 is Element of the carrier of F
r2 is Element of the carrier of F
r2 * s2 is Element of the carrier of F
s1 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
a is Element of the carrier of F
r2 * a is Element of the carrier of F
b is Element of the carrier of F
r2 * b is Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
K19( the carrier of F) is non empty set
a is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of F : (F,b₁,a) } is set
r2 is set
s1 is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
b is Element of K19( the carrier of F)
r2 is Element of K19( the carrier of F)
F is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
(F,a) is Element of K19( the carrier of F)
K19( the carrier of F) is non empty set
F is non empty associative multLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
(F,a) is Element of K19( the carrier of F)
K19( the carrier of F) is non empty set
b is Element of the carrier of F
(F,b) is Element of K19( the carrier of F)
(F,a) /\ (F,b) is Element of K19( the carrier of F)
r2 is set
s1 is Element of the carrier of F
s2 is Element of the carrier of F
s2 is Element of the carrier of F
F is non empty multLoopStr
the carrier of F is non empty set
K19( the carrier of F) is non empty set
K19(K19( the carrier of F)) is non empty set
a is Element of K19(K19( the carrier of F))
a is Element of K19(K19( the carrier of F))
b is Element of K19(K19( the carrier of F))
F is non empty multLoopStr
(F) is Element of K19(K19( the carrier of F))
the carrier of F is non empty set
K19( the carrier of F) is non empty set
K19(K19( the carrier of F)) is non empty set
1. F is Element of the carrier of F
(F,(1. F)) is Element of K19( the carrier of F)
F is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
K19( the carrier of F) is non empty set
(F) is non empty Element of K19(K19( the carrier of F))
K19(K19( the carrier of F)) is non empty set
a is Element of K19( the carrier of F)
b is Element of the carrier of F
(F,b) is non empty Element of K19( the carrier of F)
F is non empty unital associative right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
K19( the carrier of F) is non empty set
a is non empty unital associative right_unital well-unital left_unital multLoopStr
(a) is non empty Element of K19(K19( the carrier of a))
the carrier of a is non empty set
K19( the carrier of a) is non empty set
K19(K19( the carrier of a)) is non empty set
b is non empty set
r2 is set
s1 is Element of the carrier of a
(a,s1) is non empty Element of K19( the carrier of a)
r2 is set
s1 is set
s2 is Element of the carrier of a
(a,s2) is non empty Element of K19( the carrier of a)
z2 is Element of the carrier of a
(a,z2) is non empty Element of K19( the carrier of a)
r2 is set
1. a is Element of the carrier of a
(a,(1. a)) is non empty Element of K19( the carrier of a)
r2 /\ (a,(1. a)) is Element of K19( the carrier of a)
s1 is set
{s1} is non empty set
s1 is non empty set
{ b₁ where b₁ is Element of s1 : ex b₂ being non empty Element of K19( the carrier of a) st
( b₂ in b & s1 /\ b₂ = {b₁} ) } is set
1. a is Element of the carrier of a
(a,(1. a)) is non empty Element of K19( the carrier of a)
s1 /\ (a,(1. a)) is Element of K19( the carrier of a)
z2 is set
{z2} is non empty set
z1 is set
z2 is non empty set
s2 is Element of s1
{s2} is non empty set
u is non empty Element of K19( the carrier of a)
s1 /\ u is Element of K19( the carrier of a)
z2 is Element of b
{ b₁ where b₁ is Element of s1 : ex b₂ being non empty Element of K19( the carrier of a) st
( b₂ in b & s1 /\ b₂ = {b₁} ) } /\ z2 is set
s1 /\ z2 is set
z1 is set
{z1} is non empty set
s2 is set
u is Element of s1
r2 is non empty Element of K19( the carrier of a)
s1 /\ r2 is Element of K19( the carrier of a)
{u} is non empty set
z2 is non empty Element of K19( the carrier of a)
z1 is Element of z2
s2 is Element of z2
(a,z1) is non empty Element of K19( the carrier of a)
z2 /\ (a,z1) is Element of K19( the carrier of a)
u is Element of z2
{u} is non empty set
z1 is Element of the carrier of a
(a,z1) is non empty Element of K19( the carrier of a)
s2 is Element of b
z2 /\ s2 is Element of K19( the carrier of a)
u is Element of z2
{u} is non empty set
F is non empty unital associative right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
K19( the carrier of F) is non empty set
1. F is Element of the carrier of F
a is non empty (F)
b is Element of a
{ b₁ where b₁ is Element of a : not b₁ = b } is set
{(1. F)} is non empty set
{ b₁ where b₁ is Element of a : not b₁ = b } \/ {(1. F)} is non empty set
s1 is non empty set
s2 is Element of s1
z2 is Element of a
s2 is set
s2 is non empty Element of K19( the carrier of F)
z2 is Element of s2
z1 is Element of s2
s2 is Element of a
s2 is Element of a
z2 is Element of the carrier of F
z1 is Element of a
z1 is Element of s2
s2 is Element of s2
F is non empty unital associative right_unital well-unital left_unital multLoopStr
1. F is Element of the carrier of F
the carrier of F is non empty set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of a
s1 is Element of a
F is non empty unital associative right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
a is non empty (F)
b is Element of a
r2 is Element of a
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
0. F is V48(F) Element of the carrier of F
the carrier of F is non empty set
a is non empty (F)
b is Element of a
r2 is Element of the carrier of F
(0. F) * r2 is Element of the carrier of F
F is non empty unital associative right_unital well-unital left_unital multLoopStr
the carrier of F is non empty set
a is non empty (F)
b is Element of the carrier of F
r2 is non empty (F)
s1 is Element of the carrier of F
s2 is Element of r2
r2 is Element of the carrier of F
s1 is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
0. F is V48(F) Element of the carrier of F
the carrier of F is non empty set
1. F is Element of the carrier of F
a is non empty (F)
(F,a,(0. F)) is Element of the carrier of F
(F,a,(1. F)) is Element of the carrier of F
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
r2 is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of r2 is non empty set
b is Element of the carrier of F
a is non empty (F)
(F,a,b) is Element of the carrier of F
s2 is Element of the carrier of r2
s1 is non empty (r2)
(r2,s1,s2) is Element of the carrier of r2
F is non empty unital associative right_unital well-unital left_unital multLoopStr
F is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
a is non empty (F)
r2 is Element of a
b is Element of a
(F,b,r2) is Element of the carrier of F
s2 is Element of a
z2 is Element of the carrier of F
(F,b,r2) * z2 is Element of the carrier of F
r2 * (F,b,r2) is Element of the carrier of F
z2 * b is Element of the carrier of F
r2 * s2 is Element of the carrier of F
1. F is Element of the carrier of F
z1 is Element of the carrier of F
z2 * z1 is Element of the carrier of F
(z2 * b) * z1 is Element of the carrier of F
z1 * z2 is Element of the carrier of F
(z1 * z2) * b is Element of the carrier of F
1. F is Element of the carrier of F
(1. F) * b is Element of the carrier of F
r2 * (F,b,r2) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of F is non empty V12() set
a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s1 * r2 is Element of the carrier of F
s1 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(1_ F) * b is Element of the carrier of F
(1_ F) * a is Element of the carrier of F
a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
b * (0. F) is Element of the carrier of F
r2 is Element of the carrier of F
b is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
a * (0. F) is Element of the carrier of F
r2 is Element of the carrier of F
a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
a is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
b is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
the carrier of b is non empty V12() set
r2 is Element of the carrier of b
s1 is Element of the carrier of b
the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty V12() set
a is Element of the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
b is Element of the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty V12() set
a is Element of the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
b is Element of the carrier of the non empty non degenerated V46() right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
F is non empty right_complementable almost_left_invertible unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed doubleLoopStr
the carrier of F is non empty set
a is Element of the carrier of F
b is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
1_ F is Element of the carrier of F
1. F is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s1 * r2 is Element of the carrier of F
s1 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(1_ F) * b is Element of the carrier of F
(1_ F) * a is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b * (0. F) is Element of the carrier of F
r2 is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
a * (0. F) is Element of the carrier of F
r2 is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
F is non empty unital associative right_unital well-unital left_unital () multLoopStr
the carrier of F is non empty set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of a
z2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
s1 is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s2 is Element of the carrier of F
s1 * s2 is Element of the carrier of F
z2 is Element of the carrier of F
(F,a,b,r2) * z2 is Element of the carrier of F
s2 * z2 is Element of the carrier of F
s1 * (s2 * z2) is Element of the carrier of F
z1 is Element of the carrier of F
(F,a,b,r2) * z1 is Element of the carrier of F
s2 * z1 is Element of the carrier of F
s1 * (s2 * z1) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
(F,a,r2,b) is Element of the carrier of F
s2 is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
0. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
(F,a,b,(0. F)) is Element of the carrier of F
(F,a,b) is Element of the carrier of F
(F,a,(0. F),b) is Element of the carrier of F
(F,a,b) * (0. F) is Element of the carrier of F
r2 is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
0. F is V48(F) Element of the carrier of F
the carrier of F is non empty V12() set
a is non empty (F)
(F,a,(0. F),(0. F)) is Element of the carrier of F
(F,a,(0. F)) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
(F,a,b,(1. F)) is Element of the carrier of F
(F,a,(1. F),b) is Element of the carrier of F
(1. F) * b is Element of the carrier of F
r2 is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
0. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
(0. F) * s1 is Element of the carrier of F
s2 is Element of the carrier of F
(0. F) * s2 is Element of the carrier of F
(F,a,b) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
r2 is Element of the carrier of F
s1 is Element of the carrier of F
b is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
(F,a,b,s1) is Element of the carrier of F
(F,a,r2,b) is Element of the carrier of F
(F,a,s1,b) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
(F,a,(F,a,b,r2),s1) is Element of the carrier of F
(F,a,r2,s1) is Element of the carrier of F
(F,a,b,(F,a,r2,s1)) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
s1 is Element of the carrier of F
b * s1 is Element of the carrier of F
r2 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(F,a,(b * s1),(r2 * s1)) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 * (F,a,b,r2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
z1 is Element of the carrier of F
(s1 * (F,a,b,r2)) * z1 is Element of the carrier of F
(F,a,b,r2) * z1 is Element of the carrier of F
s2 is Element of the carrier of F
((s1 * (F,a,b,r2)) * z1) * s2 is Element of the carrier of F
s1 * ((F,a,b,r2) * z1) is Element of the carrier of F
(s1 * ((F,a,b,r2) * z1)) * s2 is Element of the carrier of F
s1 * b is Element of the carrier of F
u is Element of the carrier of F
((s1 * (F,a,b,r2)) * z1) * u is Element of the carrier of F
(s1 * ((F,a,b,r2) * z1)) * u is Element of the carrier of F
s1 * r2 is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(F,a,b,r2) * (1. F) is Element of the carrier of F
(0. F) * s1 is Element of the carrier of F
(F,a,(0. F),((0. F) * s1)) is Element of the carrier of F
(F,a,(0. F),(0. F)) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(F,a,b,(r2 * s1)) is Element of the carrier of F
(F,a,b,s1) is Element of the carrier of F
s1 * (F,a,b,r2) is Element of the carrier of F
b * s1 is Element of the carrier of F
(F,a,(b * s1),(r2 * s1)) is Element of the carrier of F
(F,a,b,(F,a,(b * s1),(r2 * s1))) is Element of the carrier of F
(F,a,b,(b * s1)) is Element of the carrier of F
(F,a,(F,a,b,(b * s1)),(r2 * s1)) is Element of the carrier of F
(F,a,(1. F),s1) is Element of the carrier of F
b * (F,a,(1. F),s1) is Element of the carrier of F
b * (1. F) is Element of the carrier of F
(F,a,(b * (1. F)),(b * s1)) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
0. F is V48(F) Element of the carrier of F
1. F is V48(F) Element of the carrier of F
a is non empty (F)
s1 is Element of the carrier of F
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
(F,b,s1) is Element of the carrier of F
(F,r2,s1) is Element of the carrier of F
(F,a,(F,b,s1),(F,r2,s1)) is Element of the carrier of F
(F,b,s1) * s1 is Element of the carrier of F
(F,r2,s1) * s1 is Element of the carrier of F
(F,a,((F,b,s1) * s1),((F,r2,s1) * s1)) is Element of the carrier of F
s1 * (F,a,(F,b,s1),(F,r2,s1)) is Element of the carrier of F
s1 * (1. F) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
b + (r2 * s1) is Element of the carrier of F
(F,a,(b + (r2 * s1)),s1) is Element of the carrier of F
(F,a,b,s1) is Element of the carrier of F
z2 is Element of the carrier of F
(F,a,b,s1) * z2 is Element of the carrier of F
z1 is Element of the carrier of F
(F,a,b,s1) * z1 is Element of the carrier of F
s2 is Element of the carrier of F
u is Element of the carrier of F
s2 * u is Element of the carrier of F
r2 is Element of the carrier of F
s2 * r2 is Element of the carrier of F
r2 * u is Element of the carrier of F
- (r2 * u) is Element of the carrier of F
r2 + (- (r2 * u)) is Element of the carrier of F
s2 * (r2 + (- (r2 * u))) is Element of the carrier of F
s2 * (- (r2 * u)) is Element of the carrier of F
(s2 * r2) + (s2 * (- (r2 * u))) is Element of the carrier of F
u * r2 is Element of the carrier of F
s2 * (u * r2) is Element of the carrier of F
- (s2 * (u * r2)) is Element of the carrier of F
(s2 * r2) + (- (s2 * (u * r2))) is Element of the carrier of F
s1 * r2 is Element of the carrier of F
- (s1 * r2) is Element of the carrier of F
(b + (r2 * s1)) + (- (s1 * r2)) is Element of the carrier of F
(r2 * s1) + (- (s1 * r2)) is Element of the carrier of F
b + ((r2 * s1) + (- (s1 * r2))) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
b + (0. F) is Element of the carrier of F
z1 * r2 is Element of the carrier of F
z2 + (z1 * r2) is Element of the carrier of F
(F,a,b,s1) * (z2 + (z1 * r2)) is Element of the carrier of F
(F,a,b,s1) * (z1 * r2) is Element of the carrier of F
((F,a,b,s1) * z2) + ((F,a,b,s1) * (z1 * r2)) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
r2 * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(r2 * (F,s2,(F,a,r2,s2)))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
(F,a,(F,r2,(F,a,r2,s2)),(F,s2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,(F,s2,(F,a,r2,s2)),s1) is Element of the carrier of F
u is Element of the carrier of F
(F,a,(F,s2,(F,a,r2,s2)),s1) * u is Element of the carrier of F
u * (F,a,r2,s2) is Element of the carrier of F
(F,a,(F,s2,(F,a,r2,s2)),s1) * (u * (F,a,r2,s2)) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) * (F,a,r2,s2) is Element of the carrier of F
(1. F) * (F,a,(F,s2,(F,a,r2,s2)),s1) is Element of the carrier of F
(F,a,(F,s2,(F,a,r2,s2)),(s1 * (F,r2,(F,a,r2,s2)))) is Element of the carrier of F
(F,a,(F,s2,(F,a,r2,s2)),(F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,s2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,(s1 * (F,r2,(F,a,r2,s2))),(F,s2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,r2,s2) * r2 is Element of the carrier of F
(F,a,(F,r2,(F,a,r2,s2)),b) is Element of the carrier of F
u is Element of the carrier of F
(F,a,(F,r2,(F,a,r2,s2)),b) * u is Element of the carrier of F
u * (F,a,r2,s2) is Element of the carrier of F
(F,a,(F,r2,(F,a,r2,s2)),b) * (u * (F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) * (F,a,r2,s2) is Element of the carrier of F
(1. F) * (F,a,(F,r2,(F,a,r2,s2)),b) is Element of the carrier of F
(F,a,(F,r2,(F,a,r2,s2)),(b * (F,s2,(F,a,r2,s2)))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,(b * (F,s2,(F,a,r2,s2))),(F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,r2,s2) * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),((F,a,r2,s2) * (F,r2,(F,a,r2,s2)))) is Element of the carrier of F
(1. F) * r2 is Element of the carrier of F
((1. F) * r2) * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,(F,a,r2,s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(F,a,r2,s2),(F,a,r2,s2)) * r2 is Element of the carrier of F
((F,(F,a,r2,s2),(F,a,r2,s2)) * r2) * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,((F,a,r2,s2) * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,((F,a,r2,s2) * r2),(F,a,r2,s2)) * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) * ((F,a,r2,s2) * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,b,s2) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,a,s1,r2) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,a,((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2))),((F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)))) is Element of the carrier of F
(F,a,(F,s1,(F,a,s1,r2)),(F,r2,(F,a,s1,r2))) is Element of the carrier of F
(F,a,(F,b,(F,a,b,s2)),(F,r2,(F,a,s1,r2))) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,a,s1,r2) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,a,b,s2) is Element of the carrier of F
(1. F) * (F,a,(F,b,(F,a,b,s2)),(F,r2,(F,a,s1,r2))) is Element of the carrier of F
(F,a,(F,r2,(F,a,s1,r2)),(F,b,(F,a,b,s2))) is Element of the carrier of F
(F,a,(F,s1,(F,a,s1,r2)),(F,s2,(F,a,b,s2))) is Element of the carrier of F
(F,s2,(F,a,b,s2)) * (F,a,b,s2) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) * (F,a,s1,r2) is Element of the carrier of F
(1. F) * (F,a,(F,s1,(F,a,s1,r2)),(F,s2,(F,a,b,s2))) is Element of the carrier of F
(F,a,(F,s2,(F,a,b,s2)),(F,b,(F,a,b,s2))) is Element of the carrier of F
(F,a,(F,b,(F,a,b,s2)),(F,s2,(F,a,b,s2))) is Element of the carrier of F
(F,a,((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2))),(F,r2,(F,a,s1,r2))) is Element of the carrier of F
(F,a,(F,r2,(F,a,s1,r2)),((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)))) is Element of the carrier of F
(F,a,(F,r2,(F,a,s1,r2)),(F,s1,(F,a,s1,r2))) is Element of the carrier of F
(F,a,((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2))),(F,s2,(F,a,b,s2))) is Element of the carrier of F
(F,a,(F,s2,(F,a,b,s2)),((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)))) is Element of the carrier of F
(F,a,(F,s2,(F,a,b,s2)),(F,s1,(F,a,s1,r2))) is Element of the carrier of F
F is non empty unital associative right_unital well-unital left_unital () multLoopStr
the carrier of F is non empty set
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is non empty (F)
r2 is Element of the carrier of F
s1 is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(1. F) * r2 is Element of the carrier of F
(1. F) * s1 is Element of the carrier of F
(F,a,r2,s1) is Element of the carrier of F
s2 is Element of the carrier of F
(F,b,r2,s1) is Element of the carrier of F
F is non empty unital associative right_unital well-unital left_unital () multLoopStr
the carrier of F is non empty set
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
r2 is Element of the carrier of F
s1 is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
s2 is non empty (F)
(F,s2,r2,s1) is Element of the carrier of F
(F,s2,s1,r2) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
1. F is V48(F) Element of the carrier of F
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
s1 is non empty (F)
(F,s1,b,r2) is Element of the carrier of F
F is non empty unital associative right_unital well-unital left_unital () multLoopStr_0
the carrier of F is non empty set
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
a is non empty (F)
(F,a,r2) is Element of the carrier of F
(F,a,s2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
b * s2 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(b * s2) + (r2 * s1) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
z2 is Element of the carrier of F
(b * s2) + (0. F) is Element of the carrier of F
b * (1. F) is Element of the carrier of F
z2 is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (0. F) is Element of the carrier of F
(F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
b * (F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
b * (1. F) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
z2 is Element of the carrier of F
(0. F) + (r2 * s1) is Element of the carrier of F
(1. F) * s1 is Element of the carrier of F
z2 is Element of the carrier of F
(0. F) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
s1 * (1. F) is Element of the carrier of F
z2 is Element of the carrier of F
(F,r2,(1. F)) is Element of the carrier of F
s1 * (F,r2,(1. F)) is Element of the carrier of F
(b * s2) + (s1 * (F,r2,(1. F))) is Element of the carrier of F
s1 * r2 is Element of the carrier of F
(b * s2) + (s1 * r2) is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
s2 is Element of the carrier of F
u is Element of the carrier of F
r2 is Element of the carrier of F
v is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
a is non empty (F)
(F,a,r2) is Element of the carrier of F
(F,a,s2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
r2 * s2 is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
r2 * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
(F,(r2 * (F,s2,(F,a,r2,s2))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
b * s2 is Element of the carrier of F
(F,r2,(1. F)) is Element of the carrier of F
s1 * (F,r2,(1. F)) is Element of the carrier of F
(b * s2) + (s1 * (F,r2,(1. F))) is Element of the carrier of F
s1 * r2 is Element of the carrier of F
(b * s2) + (s1 * r2) is Element of the carrier of F
- (s1 * r2) is Element of the carrier of F
- (b * s2) is Element of the carrier of F
(F,a,s2,s1) is Element of the carrier of F
(F,a,s2,(s1 * r2)) is Element of the carrier of F
(F,a,s2,r2) is Element of the carrier of F
(1. F) * s2 is Element of the carrier of F
(F,a,((1. F) * s2),(- (b * s2))) is Element of the carrier of F
- b is Element of the carrier of F
(- b) * s2 is Element of the carrier of F
(F,a,((1. F) * s2),((- b) * s2)) is Element of the carrier of F
(F,a,(1. F),(- b)) is Element of the carrier of F
s2 * (F,a,(1. F),(- b)) is Element of the carrier of F
z2 is Element of the carrier of F
(F,a,r2,b) is Element of the carrier of F
(F,a,r2,(b * s2)) is Element of the carrier of F
(1. F) * r2 is Element of the carrier of F
(F,a,((1. F) * r2),(- (s1 * r2))) is Element of the carrier of F
- s1 is Element of the carrier of F
(- s1) * r2 is Element of the carrier of F
(F,a,((1. F) * r2),((- s1) * r2)) is Element of the carrier of F
(F,a,(1. F),(- s1)) is Element of the carrier of F
r2 * (F,a,(1. F),(- s1)) is Element of the carrier of F
s2 * (1. F) is Element of the carrier of F
r2 * (1. F) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
z2 is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
z2 is Element of the carrier of F
z2 is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (0. F) is Element of the carrier of F
(F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
b * (F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
b * (1. F) is Element of the carrier of F
z2 is Element of the carrier of F
(0. F) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,(1. F),(F,a,r2,s2)) is Element of the carrier of F
s1 * (1. F) is Element of the carrier of F
z2 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
s2 is Element of the carrier of F
u is Element of the carrier of F
r2 is Element of the carrier of F
v is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,r2) is Element of the carrier of F
(F,a,s2) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
r2 * s2 is Element of the carrier of F
b * s2 is Element of the carrier of F
r2 * s1 is Element of the carrier of F
(b * s2) + (r2 * s1) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
(F,s2,(1. F)) is Element of the carrier of F
b * (F,s2,(1. F)) is Element of the carrier of F
s1 * r2 is Element of the carrier of F
(b * (F,s2,(1. F))) + (s1 * r2) is Element of the carrier of F
(F,a,((b * (F,s2,(1. F))) + (s1 * r2)),(r2 * s2)) is Element of the carrier of F
(F,r2,(1. F)) is Element of the carrier of F
s1 * (F,r2,(1. F)) is Element of the carrier of F
(b * (F,s2,(1. F))) + (s1 * (F,r2,(1. F))) is Element of the carrier of F
(F,a,((b * (F,s2,(1. F))) + (s1 * (F,r2,(1. F)))),(r2 * s2)) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
r2 * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(r2 * (F,s2,(F,a,r2,s2)))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
z2 is Element of a
z1 is Element of a
z2 * z1 is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
r2 * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,(r2 * (F,s2,(F,a,r2,s2))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(r2 * (F,s2,(F,a,r2,s2)))) is Element of the carrier of F
(F,a,(F,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))),(F,(r2 * (F,s2,(F,a,r2,s2))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)))) is Element of the carrier of F
z2 is Element of a
z1 is Element of a
(F,a,z2,z1) is Element of the carrier of F
(F,z1,(F,a,z2,z1)) is Element of the carrier of F
b * (F,z1,(F,a,z2,z1)) is Element of the carrier of F
(F,z2,(F,a,z2,z1)) is Element of the carrier of F
s1 * (F,z2,(F,a,z2,z1)) is Element of the carrier of F
(b * (F,z1,(F,a,z2,z1))) + (s1 * (F,z2,(F,a,z2,z1))) is Element of the carrier of F
(F,a,((b * (F,z1,(F,a,z2,z1))) + (s1 * (F,z2,(F,a,z2,z1)))),(F,a,z2,z1)) is Element of the carrier of F
s2 is Element of a
u is Element of a
z2 * u is Element of the carrier of F
z2 * (F,z1,(F,a,z2,z1)) is Element of the carrier of F
z2 * z1 is Element of the carrier of F
r2 is Element of a
(F,(z2 * z1),(F,a,z2,z1)) is Element of the carrier of F
(F,r2,s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
r2 * s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) * (r2 * s2) is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
b * s2 is Element of the carrier of F
s1 * r2 is Element of the carrier of F
(b * s2) + (s1 * r2) is Element of the carrier of F
(F,a,b,r2,s1,s2) * ((b * s2) + (s1 * r2)) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(F,a,s2) is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(0. F) + (s1 * r2) is Element of the carrier of F
s2 * ((0. F) + (s1 * r2)) is Element of the carrier of F
s2 * (s1 * r2) is Element of the carrier of F
(b * s2) + (0. F) is Element of the carrier of F
r2 * ((b * s2) + (0. F)) is Element of the carrier of F
r2 * (b * s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
z2 is Element of the carrier of F
(F,a,r2,s2) * z2 is Element of the carrier of F
z1 is Element of the carrier of F
(F,a,r2,s2) * z1 is Element of the carrier of F
z1 * s1 is Element of the carrier of F
z2 * b is Element of the carrier of F
(z1 * s1) + (z2 * b) is Element of the carrier of F
(F,a,r2,s2) * ((z1 * s1) + (z2 * b)) is Element of the carrier of F
(F,a,r2,s2) * (z1 * s1) is Element of the carrier of F
(F,a,r2,s2) * (z2 * b) is Element of the carrier of F
((F,a,r2,s2) * (z1 * s1)) + ((F,a,r2,s2) * (z2 * b)) is Element of the carrier of F
((F,a,r2,s2) * z1) * s1 is Element of the carrier of F
(((F,a,r2,s2) * z1) * s1) + ((F,a,r2,s2) * (z2 * b)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,(s1 * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) + (F,(s1 * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * s2) + (s1 * r2)),(F,a,r2,s2)) is Element of the carrier of F
(0. F) * (F,a,r2,s2) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(b * s2) * r2 is Element of the carrier of F
((b * s2) * r2) * s2 is Element of the carrier of F
(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
r2 * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(r2 * (F,s2,(F,a,r2,s2))) * ((b * s2) + (s1 * r2)) is Element of the carrier of F
(s1 * r2) * r2 is Element of the carrier of F
((s1 * r2) * r2) * s2 is Element of the carrier of F
(r2 * s2) * b is Element of the carrier of F
((r2 * s2) * b) * s2 is Element of the carrier of F
(r2 * s2) * s1 is Element of the carrier of F
((r2 * s2) * s1) * r2 is Element of the carrier of F
(F,(r2 * (F,s2,(F,a,r2,s2))),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
(r2 * (F,s2,(F,a,r2,s2))) * (b * s2) is Element of the carrier of F
(r2 * (F,s2,(F,a,r2,s2))) * (s1 * r2) is Element of the carrier of F
((r2 * (F,s2,(F,a,r2,s2))) * (b * s2)) + ((r2 * (F,s2,(F,a,r2,s2))) * (s1 * r2)) is Element of the carrier of F
(r2 * (F,s2,(F,a,r2,s2))) * b is Element of the carrier of F
((r2 * (F,s2,(F,a,r2,s2))) * b) * s2 is Element of the carrier of F
(((r2 * (F,s2,(F,a,r2,s2))) * b) * s2) + ((r2 * (F,s2,(F,a,r2,s2))) * (s1 * r2)) is Element of the carrier of F
(r2 * (F,s2,(F,a,r2,s2))) * s1 is Element of the carrier of F
((r2 * (F,s2,(F,a,r2,s2))) * s1) * r2 is Element of the carrier of F
(((r2 * (F,s2,(F,a,r2,s2))) * b) * s2) + (((r2 * (F,s2,(F,a,r2,s2))) * s1) * r2) is Element of the carrier of F
(F,(r2 * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(r2 * s2),(F,a,r2,s2)) * b is Element of the carrier of F
((F,(r2 * s2),(F,a,r2,s2)) * b) * s2 is Element of the carrier of F
(((F,(r2 * s2),(F,a,r2,s2)) * b) * s2) + (((r2 * (F,s2,(F,a,r2,s2))) * s1) * r2) is Element of the carrier of F
(F,(r2 * s2),(F,a,r2,s2)) * s1 is Element of the carrier of F
((F,(r2 * s2),(F,a,r2,s2)) * s1) * r2 is Element of the carrier of F
(((F,(r2 * s2),(F,a,r2,s2)) * b) * s2) + (((F,(r2 * s2),(F,a,r2,s2)) * s1) * r2) is Element of the carrier of F
(F,((r2 * s2) * b),(F,a,r2,s2)) is Element of the carrier of F
(F,((r2 * s2) * b),(F,a,r2,s2)) * s2 is Element of the carrier of F
((F,((r2 * s2) * b),(F,a,r2,s2)) * s2) + (((F,(r2 * s2),(F,a,r2,s2)) * s1) * r2) is Element of the carrier of F
(F,((r2 * s2) * s1),(F,a,r2,s2)) is Element of the carrier of F
(F,((r2 * s2) * s1),(F,a,r2,s2)) * r2 is Element of the carrier of F
((F,((r2 * s2) * b),(F,a,r2,s2)) * s2) + ((F,((r2 * s2) * s1),(F,a,r2,s2)) * r2) is Element of the carrier of F
(F,(((r2 * s2) * b) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((r2 * s2) * b) * s2),(F,a,r2,s2)) + ((F,((r2 * s2) * s1),(F,a,r2,s2)) * r2) is Element of the carrier of F
s2 * r2 is Element of the carrier of F
b * (s2 * r2) is Element of the carrier of F
(b * (s2 * r2)) * s2 is Element of the carrier of F
(F,((b * (s2 * r2)) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((r2 * s2) * s1) * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * (s2 * r2)) * s2),(F,a,r2,s2)) + (F,(((r2 * s2) * s1) * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + (F,(((r2 * s2) * s1) * r2),(F,a,r2,s2)) is Element of the carrier of F
(r2 * s2) * r2 is Element of the carrier of F
s1 * ((r2 * s2) * r2) is Element of the carrier of F
(F,(s1 * ((r2 * s2) * r2)),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + (F,(s1 * ((r2 * s2) * r2)),(F,a,r2,s2)) is Element of the carrier of F
r2 * r2 is Element of the carrier of F
(r2 * r2) * s2 is Element of the carrier of F
s1 * ((r2 * r2) * s2) is Element of the carrier of F
(F,(s1 * ((r2 * r2) * s2)),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + (F,(s1 * ((r2 * r2) * s2)),(F,a,r2,s2)) is Element of the carrier of F
s1 * (r2 * r2) is Element of the carrier of F
(s1 * (r2 * r2)) * s2 is Element of the carrier of F
(F,((s1 * (r2 * r2)) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + (F,((s1 * (r2 * r2)) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((s1 * r2) * r2) * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + (F,(((s1 * r2) * r2) * s2),(F,a,r2,s2)) is Element of the carrier of F
((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))) * (r2 * s2) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) * (r2 * s2) is Element of the carrier of F
(s1 * (F,r2,(F,a,r2,s2))) * (r2 * s2) is Element of the carrier of F
((b * (F,s2,(F,a,r2,s2))) * (r2 * s2)) + ((s1 * (F,r2,(F,a,r2,s2))) * (r2 * s2)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) * (r2 * s2) is Element of the carrier of F
((F,(b * s2),(F,a,r2,s2)) * (r2 * s2)) + ((s1 * (F,r2,(F,a,r2,s2))) * (r2 * s2)) is Element of the carrier of F
(F,(s1 * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,(s1 * r2),(F,a,r2,s2)) * (r2 * s2) is Element of the carrier of F
((F,(b * s2),(F,a,r2,s2)) * (r2 * s2)) + ((F,(s1 * r2),(F,a,r2,s2)) * (r2 * s2)) is Element of the carrier of F
(F,(b * s2),(F,a,r2,s2)) * r2 is Element of the carrier of F
((F,(b * s2),(F,a,r2,s2)) * r2) * s2 is Element of the carrier of F
(((F,(b * s2),(F,a,r2,s2)) * r2) * s2) + ((F,(s1 * r2),(F,a,r2,s2)) * (r2 * s2)) is Element of the carrier of F
(F,(s1 * r2),(F,a,r2,s2)) * r2 is Element of the carrier of F
((F,(s1 * r2),(F,a,r2,s2)) * r2) * s2 is Element of the carrier of F
(((F,(b * s2),(F,a,r2,s2)) * r2) * s2) + (((F,(s1 * r2),(F,a,r2,s2)) * r2) * s2) is Element of the carrier of F
(F,((b * s2) * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,((b * s2) * r2),(F,a,r2,s2)) * s2 is Element of the carrier of F
((F,((b * s2) * r2),(F,a,r2,s2)) * s2) + (((F,(s1 * r2),(F,a,r2,s2)) * r2) * s2) is Element of the carrier of F
(F,((s1 * r2) * r2),(F,a,r2,s2)) is Element of the carrier of F
(F,((s1 * r2) * r2),(F,a,r2,s2)) * s2 is Element of the carrier of F
((F,((b * s2) * r2),(F,a,r2,s2)) * s2) + ((F,((s1 * r2) * r2),(F,a,r2,s2)) * s2) is Element of the carrier of F
(F,(((b * s2) * r2) * s2),(F,a,r2,s2)) + ((F,((s1 * r2) * r2),(F,a,r2,s2)) * s2) is Element of the carrier of F
(F,(((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))) * (r2 * s2)),(F,a,((b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2)))),(F,a,r2,s2))) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
(F,a,r2,s2) is Element of the carrier of F
(F,s2,(F,a,r2,s2)) is Element of the carrier of F
b * (F,s2,(F,a,r2,s2)) is Element of the carrier of F
(F,r2,(F,a,r2,s2)) is Element of the carrier of F
s1 * (F,r2,(F,a,r2,s2)) is Element of the carrier of F
(b * (F,s2,(F,a,r2,s2))) + (s1 * (F,r2,(F,a,r2,s2))) is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
b is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
s1 is Element of the carrier of F
r2 is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
s2 is Element of the carrier of F
b * s1 is Element of the carrier of F
a is non empty (F)
(F,a,b,s2) is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) is Element of the carrier of F
(F,a,s1,r2) is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
z1 is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) * (F,a,s1,r2) is Element of the carrier of F
z1 is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) * (F,a,b,s2) is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
s2 is Element of the carrier of F
u is Element of the carrier of F
r2 is Element of the carrier of F
v is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
a is non empty (F)
(F,a,r2) is Element of the carrier of F
(F,a,s2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(F,a,b,s2) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,a,s1,r2) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
z2 is Element of the carrier of F
z1 is Element of the carrier of F
s2 is Element of the carrier of F
u is Element of the carrier of F
r2 is Element of the carrier of F
v is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
(F,a,s2) is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,s1,r2) is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,b,s2) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,s2,(F,a,b,s2)) * (F,r2,(F,a,s1,r2)) is Element of the carrier of F
b * s1 is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * s1 is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
z1 is Element of a
z2 is Element of a
(F,z1,z2) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)) is Element of the carrier of F
b * s1 is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
b * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
z1 is Element of a
z2 is Element of a
(F,z1,z2) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,a,(F,a,b,r2,s1,s2),(F,a,b,r2,s1,s2)) is Element of the carrier of F
s2 is Element of a
z1 is Element of a
(F,s2,z1) is Element of the carrier of F
r2 is Element of a
z2 is Element of a
(F,r2,z2) is Element of the carrier of F
v is Element of a
u is Element of a
v * u is Element of the carrier of F
F is non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like () doubleLoopStr
the carrier of F is non empty V12() set
a is non empty (F)
b is Element of the carrier of F
r2 is Element of the carrier of F
s1 is Element of the carrier of F
s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
r2 * s2 is Element of the carrier of F
(F,a,b,r2,s1,s2) * (r2 * s2) is Element of the carrier of F
(F,a,b,r2,s1,s2) is Element of the carrier of F
b * s1 is Element of the carrier of F
(F,a,b,r2,s1,s2) * (b * s1) is Element of the carrier of F
(F,a,b,r2) is Element of the carrier of F
1. F is V48(F) Element of the carrier of F
0. F is V48(F) Element of the carrier of F
(F,a,b,s2) is Element of the carrier of F
(F,a,r2) is Element of the carrier of F
(F,a,s1,s2) is Element of the carrier of F
(F,a,s1,r2) is Element of the carrier of F
(F,a,s2) is Element of the carrier of F
(F,a,b,r2,s1,s2) * (0. F) is Element of the carrier of F
(F,a,b,r2,s1,s2) * (0. F) is Element of the carrier of F
(b * s1) * s2 is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) * (r2 * s2) is Element of the carrier of F
(F,(b * s1),(F,a,b,s2)) * s2 is Element of the carrier of F
(F,((b * s1) * s2),(F,a,b,s2)) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
s2 * b is Element of the carrier of F
(s2 * b) * s1 is Element of the carrier of F
(F,s2,(F,a,b,s2)) * (b * s1) is Element of the carrier of F
(F,s2,(F,a,b,s2)) * b is Element of the carrier of F
((F,s2,(F,a,b,s2)) * b) * s1 is Element of the carrier of F
(F,(s2 * b),(F,a,b,s2)) is Element of the carrier of F
(F,(s2 * b),(F,a,b,s2)) * s1 is Element of the carrier of F
(F,((s2 * b) * s1),(F,a,b,s2)) is Element of the carrier of F
s1 * b is Element of the carrier of F
(s1 * b) * r2 is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) * (r2 * s2) is Element of the carrier of F
(F,(b * s1),(F,a,s1,r2)) * r2 is Element of the carrier of F
(b * s1) * r2 is Element of the carrier of F
(F,((b * s1) * r2),(F,a,s1,r2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
r2 * b is Element of the carrier of F
(r2 * b) * s1 is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (b * s1) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * b is Element of the carrier of F
((F,r2,(F,a,s1,r2)) * b) * s1 is Element of the carrier of F
(F,(r2 * b),(F,a,s1,r2)) is Element of the carrier of F
(F,(r2 * b),(F,a,s1,r2)) * s1 is Element of the carrier of F
(F,((r2 * b) * s1),(F,a,s1,r2)) is Element of the carrier of F
(F,a,s1,r2) * (F,a,b,s2) is Element of the carrier of F
(r2 * s2) * b is Element of the carrier of F
((r2 * s2) * b) * s1 is Element of the carrier of F
(F,a,b,s2) * (F,a,s1,r2) is Element of the carrier of F
(b * s1) * r2 is Element of the carrier of F
((b * s1) * r2) * s2 is Element of the carrier of F
(F,r2,(F,a,s1,r2)) is Element of the carrier of F
(F,s2,(F,a,b,s2)) is Element of the carrier of F
(F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2)) is Element of the carrier of F
((F,r2,(F,a,s1,r2)) * (F,s2,(F,a,b,s2))) * (b * s1) is Element of the carrier of F
(F,(r2 * s2),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
(F,(r2 * s2),((F,a,s1,r2) * (F,a,b,s2))) * (b * s1) is Element of the carrier of F
(F,(r2 * s2),((F,a,s1,r2) * (F,a,b,s2))) * b is Element of the carrier of F
((F,(r2 * s2),((F,a,s1,r2) * (F,a,b,s2))) * b) * s1 is Element of the carrier of F
(F,((r2 * s2) * b),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
(F,((r2 * s2) * b),((F,a,s1,r2) * (F,a,b,s2))) * s1 is Element of the carrier of F
(F,(((r2 * s2) * b) * s1),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
(r2 * s2) * s1 is Element of the carrier of F
b * ((r2 * s2) * s1) is Element of the carrier of F
(F,(b * ((r2 * s2) * s1)),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
s1 * r2 is Element of the carrier of F
(s1 * r2) * s2 is Element of the carrier of F
b * ((s1 * r2) * s2) is Element of the carrier of F
(F,(b * ((s1 * r2) * s2)),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
b * (s1 * r2) is Element of the carrier of F
(b * (s1 * r2)) * s2 is Element of the carrier of F
(F,((b * (s1 * r2)) * s2),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
(F,(((b * s1) * r2) * s2),((F,a,s1,r2) * (F,a,b,s2))) is Element of the carrier of F
(F,b,(F,a,b,s2)) is Element of the carrier of F
(F,s1,(F,a,s1,r2)) is Element of the carrier of F
(F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2)) is Element of the carrier of F
((F,b,(F,a,b,s2)) * (F,s1,(F,a,s1,r2))) * (r2 * s2) is Element of the carrier of F
(F,(b * s1),((F,a,b,s2) * (F,a,s1,r2))) is Element of the carrier of F
(F,(b * s1),((F,a,b,s2) * (F,a,s1,r2))) * (r2 * s2) is Element of the carrier of F
(F,(b * s1),((F,a,b,s2) * (F,a,s1,r2))) * r2 is Element of the carrier of F
((F,(b * s1),((F,a,b,s2) * (F,a,s1,r2))) * r2) * s2 is Element of the carrier of F
(F,((b * s1) * r2),((F,a,b,s2) * (F,a,s1,r2))) is Element of the carrier of F
(F,((b * s1) * r2),((F,a,b,s2) * (F,a,s1,r2))) * s2 is Element of the carrier of F
(F,(((b * s1) * r2) * s2),((F,a,b,s2) * (F,a,s1,r2))) is Element of the carrier of F
F is non empty right_complementable right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of F is non empty set
r2 is non empty right_complementable right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of r2 is non empty set
a is Element of the carrier of F
- a is Element of the carrier of F
b is Element of the carrier of F
(- a) * b is Element of the carrier of F
a * b is Element of the carrier of F
- (a * b) is Element of the carrier of F
s1 is Element of the carrier of r2
s2 is Element of the carrier of r2
- s2 is Element of the carrier of r2
s1 * (- s2) is Element of the carrier of r2
s1 * s2 is Element of the carrier of r2
- (s1 * s2) is Element of the carrier of r2
F is non empty right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed () doubleLoopStr
the carrier of F is non empty set
0. F is V48(F) Element of the carrier of F
a is Element of the carrier of F
b is Element of the carrier of F
a " is Element of the carrier of F
b " is Element of the carrier of F
(a ") * (b ") is Element of the carrier of F
b * a is Element of the carrier of F
(b * a) " is Element of the carrier of F
(b * a) * ((a ") * (b ")) is Element of the carrier of F
(b * a) * (a ") is Element of the carrier of F
((b * a) * (a ")) * (b ") is Element of the carrier of F
a * (a ") is Element of the carrier of F
b * (a * (a ")) is Element of the carrier of F
(b * (a * (a "))) * (b ") is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is Element of the carrier of F
b * (1_ F) is Element of the carrier of F
(b * (1_ F)) * (b ") is Element of the carrier of F
b * (b ") is Element of the carrier of F