:: 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

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

( b

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

( b

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

{(1. F)} is non empty set

{ b

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 *