:: EC_PF_1 semantic presentation

REAL is non empty non trivial non finite V117() V118() V119() V123() set

NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V117() V118() V119() V120() V121() V122() V123() Element of bool REAL

bool REAL is non empty non trivial non finite set

K649() is strict doubleLoopStr

the carrier of K649() is set

COMPLEX is non empty non trivial non finite V117() V123() set

NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V117() V118() V119() V120() V121() V122() V123() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

RAT is non empty non trivial non finite V117() V118() V119() V120() V123() set

INT is non empty non trivial non finite V117() V118() V119() V120() V121() V123() set

[:REAL,REAL:] is non empty non trivial V35() V36() V37() non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

K357() is non empty strict multMagma

the carrier of K357() is non empty set

INT.Ring is non empty non degenerated non trivial non finite left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V181() doubleLoopStr

addint is Relation-like [:INT,INT:] -defined INT -valued Function-like quasi_total V35() V36() V37() Element of bool [:[:INT,INT:],INT:]

[:INT,INT:] is non empty non trivial RAT -valued INT -valued V35() V36() V37() non finite set

[:[:INT,INT:],INT:] is non empty non trivial RAT -valued INT -valued V35() V36() V37() non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

multint is Relation-like [:INT,INT:] -defined INT -valued Function-like quasi_total V35() V36() V37() Element of bool [:[:INT,INT:],INT:]

1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal V113() V117() V118() V119() V120() V121() V122() Element of NAT

K633(1,INT) is V11() V12() integer ext-real V113() Element of INT

0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative finite V49() cardinal {} -element V113() V117() V118() V119() V120() V121() V122() V123() Element of NAT

{} is empty V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative finite V49() cardinal {} -element V117() V118() V119() V120() V121() V122() V123() set

K633(0,INT) is V11() V12() integer ext-real V113() Element of INT

doubleLoopStr(# INT,addint,multint,K633(1,INT),K633(0,INT) #) is non empty non trivial strict doubleLoopStr

the carrier of INT.Ring is non empty non trivial non finite V117() V118() V119() V120() V121() set

[: the carrier of INT.Ring,NAT:] is non empty non trivial RAT -valued INT -valued V35() V36() V37() V38() non finite set

bool [: the carrier of INT.Ring,NAT:] is non empty non trivial non finite set

{{},1} is non empty finite V49() V117() V118() V119() V120() V121() V122() set

K455() is set

bool K455() is non empty set

K456() is Element of bool K455()

2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal V113() V117() V118() V119() V120() V121() V122() Element of NAT

[:NAT,REAL:] is non empty non trivial V35() V36() V37() non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

1 -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT

NAT * is functional FinSequence-membered FinSequenceSet of NAT

{ b

[:COMPLEX,COMPLEX:] is non empty non trivial V35() non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V35() non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is non empty non trivial V35() V36() V37() non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is non empty non trivial RAT -valued V35() V36() V37() non finite set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is non empty non trivial RAT -valued V35() V36() V37() non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

bool [:INT,INT:] is non empty non trivial non finite set

[:NAT,NAT:] is non empty non trivial RAT -valued INT -valued V35() V36() V37() V38() non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial RAT -valued INT -valued V35() V36() V37() V38() non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

bool the carrier of K649() is non empty set

[:NAT, the carrier of K649():] is set

bool [:NAT, the carrier of K649():] is non empty set

bool (bool REAL) is non empty non trivial non finite set

K155(0,1,2) is non empty finite V117() V118() V119() V120() V121() V122() set

[:K155(0,1,2),K155(0,1,2):] is non empty RAT -valued INT -valued V35() V36() V37() V38() finite set

[:[:K155(0,1,2),K155(0,1,2):],K155(0,1,2):] is non empty RAT -valued INT -valued V35() V36() V37() V38() finite set

bool [:[:K155(0,1,2),K155(0,1,2):],K155(0,1,2):] is non empty finite V49() set

bool [:K155(0,1,2),K155(0,1,2):] is non empty finite V49() set

Z_3 is strict doubleLoopStr

add3 is Relation-like [:K155(0,1,2),K155(0,1,2):] -defined K155(0,1,2) -valued Function-like quasi_total V35() V36() V37() V38() finite Element of bool [:[:K155(0,1,2),K155(0,1,2):],K155(0,1,2):]

mult3 is Relation-like [:K155(0,1,2),K155(0,1,2):] -defined K155(0,1,2) -valued Function-like quasi_total V35() V36() V37() V38() finite Element of bool [:[:K155(0,1,2),K155(0,1,2):],K155(0,1,2):]

unit3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal V113() Element of K155(0,1,2)

zero3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal V113() Element of K155(0,1,2)

doubleLoopStr(# K155(0,1,2),add3,mult3,unit3,zero3 #) is non empty strict doubleLoopStr

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of p is non empty non trivial set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p || the carrier of p is set

the addF of p | [: the carrier of p, the carrier of p:] is Relation-like set

the multF of p || the carrier of p is set

the multF of p | [: the carrier of p, the carrier of p:] is Relation-like set

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the carrier of p is non empty non trivial set

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the addF of p || the carrier of p is set

the addF of p | [: the carrier of p, the carrier of p:] is Relation-like set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the multF of p || the carrier of p is set

the multF of p | [: the carrier of p, the carrier of p:] is Relation-like set

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of p is non empty non trivial set

bool the carrier of p is non empty set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

a is non empty doubleLoopStr

the carrier of a is non empty set

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of p || the carrier of a is set

the addF of p | [: the carrier of a, the carrier of a:] is Relation-like set

the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

the multF of p || the carrier of a is set

the multF of p | [: the carrier of a, the carrier of a:] is Relation-like set

1. a is Element of the carrier of a

the OneF of a is Element of the carrier of a

0. a is V61(a) Element of the carrier of a

the ZeroF of a is Element of the carrier of a

F1 is Element of the carrier of a

F2 is Element of the carrier of a

F1 * F2 is Element of the carrier of a

the multF of a . (F1,F2) is Element of the carrier of a

[F1,F2] is V26() set

{F1,F2} is non empty finite set

{F1} is non empty trivial finite 1 -element set

{{F1,F2},{F1}} is non empty finite V49() set

the multF of a . [F1,F2] is set

[F1,F2] is V26() Element of [: the carrier of a, the carrier of a:]

the multF of p . [F1,F2] is set

the multF of p . (F1,F2) is set

the multF of p . [F1,F2] is set

F1 is Element of the carrier of a

F2 is Element of the carrier of a

F1 + F2 is Element of the carrier of a

the addF of a . (F1,F2) is Element of the carrier of a

[F1,F2] is V26() set

{F1,F2} is non empty finite set

{F1} is non empty trivial finite 1 -element set

{{F1,F2},{F1}} is non empty finite V49() set

the addF of a . [F1,F2] is set

[F1,F2] is V26() Element of [: the carrier of a, the carrier of a:]

the addF of p . [F1,F2] is set

the addF of p . (F1,F2) is set

the addF of p . [F1,F2] is set

X is Element of the carrier of a

Y is Element of the carrier of a

X + Y is Element of the carrier of a

the addF of a . (X,Y) is Element of the carrier of a

[X,Y] is V26() set

{X,Y} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,Y},{X}} is non empty finite V49() set

the addF of a . [X,Y] is set

n1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

n1 + n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n1,n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n1,n] is V26() set

{n1,n} is non empty finite set

{n1} is non empty trivial finite 1 -element set

{{n1,n},{n1}} is non empty finite V49() set

the addF of p . [n1,n] is set

Y + X is Element of the carrier of a

the addF of a . (Y,X) is Element of the carrier of a

[Y,X] is V26() set

{Y,X} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,X},{Y}} is non empty finite V49() set

the addF of a . [Y,X] is set

n + n1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n,n1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n,n1] is V26() set

{n,n1} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,n1},{n}} is non empty finite V49() set

the addF of p . [n,n1] is set

X is Element of the carrier of a

Y is Element of the carrier of a

n1 is Element of the carrier of a

Y + n1 is Element of the carrier of a

the addF of a . (Y,n1) is Element of the carrier of a

[Y,n1] is V26() set

{Y,n1} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,n1},{Y}} is non empty finite V49() set

the addF of a . [Y,n1] is set

X + (Y + n1) is Element of the carrier of a

the addF of a . (X,(Y + n1)) is Element of the carrier of a

[X,(Y + n1)] is V26() set

{X,(Y + n1)} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,(Y + n1)},{X}} is non empty finite V49() set

the addF of a . [X,(Y + n1)] is set

n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n,(Y + n1)) is set

[n,(Y + n1)] is V26() set

{n,(Y + n1)} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,(Y + n1)},{n}} is non empty finite V49() set

the addF of p . [n,(Y + n1)] is set

y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

y1 + a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (y1,a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[y1,a1] is V26() set

{y1,a1} is non empty finite set

{y1} is non empty trivial finite 1 -element set

{{y1,a1},{y1}} is non empty finite V49() set

the addF of p . [y1,a1] is set

n + (y1 + a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n,(y1 + a1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n,(y1 + a1)] is V26() set

{n,(y1 + a1)} is non empty finite set

{{n,(y1 + a1)},{n}} is non empty finite V49() set

the addF of p . [n,(y1 + a1)] is set

X + Y is Element of the carrier of a

the addF of a . (X,Y) is Element of the carrier of a

[X,Y] is V26() set

{X,Y} is non empty finite set

{{X,Y},{X}} is non empty finite V49() set

the addF of a . [X,Y] is set

(X + Y) + n1 is Element of the carrier of a

the addF of a . ((X + Y),n1) is Element of the carrier of a

[(X + Y),n1] is V26() set

{(X + Y),n1} is non empty finite set

{(X + Y)} is non empty trivial finite 1 -element set

{{(X + Y),n1},{(X + Y)}} is non empty finite V49() set

the addF of a . [(X + Y),n1] is set

the addF of p . ((X + Y),a1) is set

[(X + Y),a1] is V26() set

{(X + Y),a1} is non empty finite set

{{(X + Y),a1},{(X + Y)}} is non empty finite V49() set

the addF of p . [(X + Y),a1] is set

n + y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n,y1] is V26() set

{n,y1} is non empty finite set

{{n,y1},{n}} is non empty finite V49() set

the addF of p . [n,y1] is set

(n + y1) + a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . ((n + y1),a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(n + y1),a1] is V26() set

{(n + y1),a1} is non empty finite set

{(n + y1)} is non empty trivial finite 1 -element set

{{(n + y1),a1},{(n + y1)}} is non empty finite V49() set

the addF of p . [(n + y1),a1] is set

X is Element of the carrier of a

X + (0. a) is Element of the carrier of a

the addF of a . (X,(0. a)) is Element of the carrier of a

[X,(0. a)] is V26() set

{X,(0. a)} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,(0. a)},{X}} is non empty finite V49() set

the addF of a . [X,(0. a)] is set

Y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

Y + (0. p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (Y,(0. p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[Y,(0. p)] is V26() set

{Y,(0. p)} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,(0. p)},{Y}} is non empty finite V49() set

the addF of p . [Y,(0. p)] is set

n1 is Element of the carrier of a

X is Element of the carrier of a

Y is Element of the carrier of a

Y * n1 is Element of the carrier of a

the multF of a . (Y,n1) is Element of the carrier of a

[Y,n1] is V26() set

{Y,n1} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,n1},{Y}} is non empty finite V49() set

the multF of a . [Y,n1] is set

X * (Y * n1) is Element of the carrier of a

the multF of a . (X,(Y * n1)) is Element of the carrier of a

[X,(Y * n1)] is V26() set

{X,(Y * n1)} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,(Y * n1)},{X}} is non empty finite V49() set

the multF of a . [X,(Y * n1)] is set

the multF of p . (X,(Y * n1)) is set

the multF of p . [X,(Y * n1)] is set

y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

a1 * n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (a1,n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[a1,n] is V26() set

{a1,n} is non empty finite set

{a1} is non empty trivial finite 1 -element set

{{a1,n},{a1}} is non empty finite V49() set

the multF of p . [a1,n] is set

y1 * (a1 * n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (y1,(a1 * n)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[y1,(a1 * n)] is V26() set

{y1,(a1 * n)} is non empty finite set

{y1} is non empty trivial finite 1 -element set

{{y1,(a1 * n)},{y1}} is non empty finite V49() set

the multF of p . [y1,(a1 * n)] is set

X * Y is Element of the carrier of a

the multF of a . (X,Y) is Element of the carrier of a

[X,Y] is V26() set

{X,Y} is non empty finite set

{{X,Y},{X}} is non empty finite V49() set

the multF of a . [X,Y] is set

y1 * a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (y1,a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[y1,a1] is V26() set

{y1,a1} is non empty finite set

{{y1,a1},{y1}} is non empty finite V49() set

the multF of p . [y1,a1] is set

(X * Y) * n1 is Element of the carrier of a

the multF of a . ((X * Y),n1) is Element of the carrier of a

[(X * Y),n1] is V26() set

{(X * Y),n1} is non empty finite set

{(X * Y)} is non empty trivial finite 1 -element set

{{(X * Y),n1},{(X * Y)}} is non empty finite V49() set

the multF of a . [(X * Y),n1] is set

(y1 * a1) * n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . ((y1 * a1),n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(y1 * a1),n] is V26() set

{(y1 * a1),n} is non empty finite set

{(y1 * a1)} is non empty trivial finite 1 -element set

{{(y1 * a1),n},{(y1 * a1)}} is non empty finite V49() set

the multF of p . [(y1 * a1),n] is set

X is Element of the carrier of a

X * (1. a) is Element of the carrier of a

the multF of a . (X,(1. a)) is Element of the carrier of a

[X,(1. a)] is V26() set

{X,(1. a)} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,(1. a)},{X}} is non empty finite V49() set

the multF of a . [X,(1. a)] is set

Y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

Y * (1. p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (Y,(1. p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[Y,(1. p)] is V26() set

{Y,(1. p)} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,(1. p)},{Y}} is non empty finite V49() set

the multF of p . [Y,(1. p)] is set

(1. a) * X is Element of the carrier of a

the multF of a . ((1. a),X) is Element of the carrier of a

[(1. a),X] is V26() set

{(1. a),X} is non empty finite set

{(1. a)} is non empty trivial finite 1 -element set

{{(1. a),X},{(1. a)}} is non empty finite V49() set

the multF of a . [(1. a),X] is set

(1. p) * Y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . ((1. p),Y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(1. p),Y] is V26() set

{(1. p),Y} is non empty finite set

{(1. p)} is non empty trivial finite 1 -element set

{{(1. p),Y},{(1. p)}} is non empty finite V49() set

the multF of p . [(1. p),Y] is set

Y is Element of the carrier of a

n1 is Element of the carrier of a

X is Element of the carrier of a

Y + n1 is Element of the carrier of a

the addF of a . (Y,n1) is Element of the carrier of a

[Y,n1] is V26() set

{Y,n1} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,n1},{Y}} is non empty finite V49() set

the addF of a . [Y,n1] is set

(Y + n1) * X is Element of the carrier of a

the multF of a . ((Y + n1),X) is Element of the carrier of a

[(Y + n1),X] is V26() set

{(Y + n1),X} is non empty finite set

{(Y + n1)} is non empty trivial finite 1 -element set

{{(Y + n1),X},{(Y + n1)}} is non empty finite V49() set

the multF of a . [(Y + n1),X] is set

the multF of p . ((Y + n1),X) is set

the multF of p . [(Y + n1),X] is set

n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

n + y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (n,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n,y1] is V26() set

{n,y1} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,y1},{n}} is non empty finite V49() set

the addF of p . [n,y1] is set

a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

(n + y1) * a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . ((n + y1),a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(n + y1),a1] is V26() set

{(n + y1),a1} is non empty finite set

{(n + y1)} is non empty trivial finite 1 -element set

{{(n + y1),a1},{(n + y1)}} is non empty finite V49() set

the multF of p . [(n + y1),a1] is set

n * a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (n,a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[n,a1] is V26() set

{n,a1} is non empty finite set

{{n,a1},{n}} is non empty finite V49() set

the multF of p . [n,a1] is set

y1 * a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (y1,a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[y1,a1] is V26() set

{y1,a1} is non empty finite set

{y1} is non empty trivial finite 1 -element set

{{y1,a1},{y1}} is non empty finite V49() set

the multF of p . [y1,a1] is set

(n * a1) + (y1 * a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . ((n * a1),(y1 * a1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(n * a1),(y1 * a1)] is V26() set

{(n * a1),(y1 * a1)} is non empty finite set

{(n * a1)} is non empty trivial finite 1 -element set

{{(n * a1),(y1 * a1)},{(n * a1)}} is non empty finite V49() set

the addF of p . [(n * a1),(y1 * a1)] is set

n1 * X is Element of the carrier of a

the multF of a . (n1,X) is Element of the carrier of a

[n1,X] is V26() set

{n1,X} is non empty finite set

{n1} is non empty trivial finite 1 -element set

{{n1,X},{n1}} is non empty finite V49() set

the multF of a . [n1,X] is set

the addF of p . (( the multF of p . (n,a1)),(n1 * X)) is set

[( the multF of p . (n,a1)),(n1 * X)] is V26() set

{( the multF of p . (n,a1)),(n1 * X)} is non empty finite set

{( the multF of p . (n,a1))} is non empty trivial finite 1 -element set

{{( the multF of p . (n,a1)),(n1 * X)},{( the multF of p . (n,a1))}} is non empty finite V49() set

the addF of p . [( the multF of p . (n,a1)),(n1 * X)] is set

Y * X is Element of the carrier of a

the multF of a . (Y,X) is Element of the carrier of a

[Y,X] is V26() set

{Y,X} is non empty finite set

{{Y,X},{Y}} is non empty finite V49() set

the multF of a . [Y,X] is set

the addF of p . ((Y * X),(n1 * X)) is set

[(Y * X),(n1 * X)] is V26() set

{(Y * X),(n1 * X)} is non empty finite set

{(Y * X)} is non empty trivial finite 1 -element set

{{(Y * X),(n1 * X)},{(Y * X)}} is non empty finite V49() set

the addF of p . [(Y * X),(n1 * X)] is set

X * (Y + n1) is Element of the carrier of a

the multF of a . (X,(Y + n1)) is Element of the carrier of a

[X,(Y + n1)] is V26() set

{X,(Y + n1)} is non empty finite set

{X} is non empty trivial finite 1 -element set

{{X,(Y + n1)},{X}} is non empty finite V49() set

the multF of a . [X,(Y + n1)] is set

the multF of p . (X,(Y + n1)) is set

the multF of p . [X,(Y + n1)] is set

a1 * (n + y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (a1,(n + y1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[a1,(n + y1)] is V26() set

{a1,(n + y1)} is non empty finite set

{a1} is non empty trivial finite 1 -element set

{{a1,(n + y1)},{a1}} is non empty finite V49() set

the multF of p . [a1,(n + y1)] is set

a1 * n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (a1,n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[a1,n] is V26() set

{a1,n} is non empty finite set

{{a1,n},{a1}} is non empty finite V49() set

the multF of p . [a1,n] is set

a1 * y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (a1,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[a1,y1] is V26() set

{a1,y1} is non empty finite set

{{a1,y1},{a1}} is non empty finite V49() set

the multF of p . [a1,y1] is set

(a1 * n) + (a1 * y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . ((a1 * n),(a1 * y1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[(a1 * n),(a1 * y1)] is V26() set

{(a1 * n),(a1 * y1)} is non empty finite set

{(a1 * n)} is non empty trivial finite 1 -element set

{{(a1 * n),(a1 * y1)},{(a1 * n)}} is non empty finite V49() set

the addF of p . [(a1 * n),(a1 * y1)] is set

the multF of p . (X,n) is set

[X,n] is V26() set

{X,n} is non empty finite set

{{X,n},{X}} is non empty finite V49() set

the multF of p . [X,n] is set

X * n1 is Element of the carrier of a

the multF of a . (X,n1) is Element of the carrier of a

[X,n1] is V26() set

{X,n1} is non empty finite set

{{X,n1},{X}} is non empty finite V49() set

the multF of a . [X,n1] is set

the addF of p . (( the multF of p . (X,n)),(X * n1)) is set

[( the multF of p . (X,n)),(X * n1)] is V26() set

{( the multF of p . (X,n)),(X * n1)} is non empty finite set

{( the multF of p . (X,n))} is non empty trivial finite 1 -element set

{{( the multF of p . (X,n)),(X * n1)},{( the multF of p . (X,n))}} is non empty finite V49() set

the addF of p . [( the multF of p . (X,n)),(X * n1)] is set

X * Y is Element of the carrier of a

the multF of a . (X,Y) is Element of the carrier of a

[X,Y] is V26() set

{X,Y} is non empty finite set

{{X,Y},{X}} is non empty finite V49() set

the multF of a . [X,Y] is set

the addF of p . ((X * Y),(X * n1)) is set

[(X * Y),(X * n1)] is V26() set

{(X * Y),(X * n1)} is non empty finite set

{(X * Y)} is non empty trivial finite 1 -element set

{{(X * Y),(X * n1)},{(X * Y)}} is non empty finite V49() set

the addF of p . [(X * Y),(X * n1)] is set

(X * Y) + (X * n1) is Element of the carrier of a

the addF of a . ((X * Y),(X * n1)) is Element of the carrier of a

the addF of a . [(X * Y),(X * n1)] is set

(Y * X) + (n1 * X) is Element of the carrier of a

the addF of a . ((Y * X),(n1 * X)) is Element of the carrier of a

the addF of a . [(Y * X),(n1 * X)] is set

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

[#] p is non empty non proper Element of bool the carrier of p

the carrier of p is non empty non trivial set

bool the carrier of p is non empty set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the addF of p || ([#] p) is set

[:([#] p),([#] p):] is non empty set

the addF of p | [:([#] p),([#] p):] is Relation-like set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the multF of p || ([#] p) is set

the multF of p | [:([#] p),([#] p):] is Relation-like set

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is non empty non trivial strict doubleLoopStr

0. doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is V61( doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)) Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is non empty non trivial set

the ZeroF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

1. doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the OneF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

L is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

F is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

pp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

F + pp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the addF of p . (F,pp) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[F,pp] is V26() set

{F,pp} is non empty finite set

{F} is non empty trivial finite 1 -element set

{{F,pp},{F}} is non empty finite V49() set

the addF of p . [F,pp] is set

FF is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

L + FF is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the addF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Relation-like [: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] -defined the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) -valued Function-like quasi_total Element of bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):]

[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

[:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

the addF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . (L,FF) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

[L,FF] is V26() set

{L,FF} is non empty finite set

{L} is non empty trivial finite 1 -element set

{{L,FF},{L}} is non empty finite V49() set

the addF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . [L,FF] is set

L is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

F is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

L * F is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Relation-like [: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] -defined the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) -valued Function-like quasi_total Element of bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):]

[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

[:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . (L,F) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

[L,F] is V26() set

{L,F} is non empty finite set

{L} is non empty trivial finite 1 -element set

{{L,F},{L}} is non empty finite V49() set

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . [L,F] is set

F * L is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . (F,L) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

[F,L] is V26() set

{F,L} is non empty finite set

{F} is non empty trivial finite 1 -element set

{{F,L},{F}} is non empty finite V49() set

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . [F,L] is set

pp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

FF is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

pp * FF is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (pp,FF) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[pp,FF] is V26() set

{pp,FF} is non empty finite set

{pp} is non empty trivial finite 1 -element set

{{pp,FF},{pp}} is non empty finite V49() set

the multF of p . [pp,FF] is set

FF * pp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (FF,pp) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[FF,pp] is V26() set

{FF,pp} is non empty finite set

{FF} is non empty trivial finite 1 -element set

{{FF,pp},{FF}} is non empty finite V49() set

the multF of p . [FF,pp] is set

L is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

F is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

pp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

pp * F is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the multF of p . (pp,F) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

[pp,F] is V26() set

{pp,F} is non empty finite set

{pp} is non empty trivial finite 1 -element set

{{pp,F},{pp}} is non empty finite V49() set

the multF of p . [pp,F] is set

FF is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

FF * L is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) is Relation-like [: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] -defined the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) -valued Function-like quasi_total Element of bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):]

[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

[:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

bool [:[: the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #), the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):], the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #):] is non empty set

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . (FF,L) is Element of the carrier of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #)

[FF,L] is V26() set

{FF,L} is non empty finite set

{FF} is non empty trivial finite 1 -element set

{{FF,L},{FF}} is non empty finite V49() set

the multF of doubleLoopStr(# the carrier of p, the addF of p, the multF of p,(1. p),(0. p) #) . [FF,L] is set

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of p is non empty non trivial set

the carrier of a is non empty non trivial set

b is set

b is set

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of p is non empty non trivial set

the carrier of a is non empty non trivial set

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a || the carrier of p is set

[: the carrier of p, the carrier of p:] is non empty set

the addF of a | [: the carrier of p, the carrier of p:] is Relation-like set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

the multF of a || the carrier of p is set

the multF of a | [: the carrier of p, the carrier of p:] is Relation-like set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

1. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the OneF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

b is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of p is non empty non trivial set

the carrier of a is non empty non trivial set

the carrier of b is non empty non trivial set

the addF of b is Relation-like [: the carrier of b, the carrier of b:] -defined the carrier of b -valued Function-like quasi_total Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]

[: the carrier of b, the carrier of b:] is non empty set

[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set

bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set

the multF of b is Relation-like [: the carrier of b, the carrier of b:] -defined the carrier of b -valued Function-like quasi_total Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]

[: the carrier of p, the carrier of p:] is non empty set

[: the carrier of a, the carrier of a:] is non empty set

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of b || the carrier of a is set

the addF of b | [: the carrier of a, the carrier of a:] is Relation-like set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the addF of a || the carrier of p is set

the addF of a | [: the carrier of p, the carrier of p:] is Relation-like set

the addF of b || the carrier of p is set

the addF of b | [: the carrier of p, the carrier of p:] is Relation-like set

the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

the multF of b || the carrier of a is set

the multF of b | [: the carrier of a, the carrier of a:] is Relation-like set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the multF of a || the carrier of p is set

the multF of a | [: the carrier of p, the carrier of p:] is Relation-like set

the multF of b || the carrier of p is set

the multF of b | [: the carrier of p, the carrier of p:] is Relation-like set

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

1. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the OneF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

1. b is V61(b) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

the OneF of b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

0. b is V61(b) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

the ZeroF of b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

the carrier of a is non empty non trivial set

b is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

the carrier of b is non empty non trivial set

the addF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the carrier of p is non empty non trivial set

[: the carrier of p, the carrier of p:] is non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of a, the carrier of a:] is non empty set

[: the carrier of b, the carrier of b:] is non empty set

the addF of b is Relation-like [: the carrier of b, the carrier of b:] -defined the carrier of b -valued Function-like quasi_total Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]

[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set

bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set

the addF of p || the carrier of b is set

the addF of p | [: the carrier of b, the carrier of b:] is Relation-like set

the addF of b || the carrier of a is set

the addF of b | [: the carrier of a, the carrier of a:] is Relation-like set

the addF of p || the carrier of a is set

the addF of p | [: the carrier of a, the carrier of a:] is Relation-like set

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the multF of b is Relation-like [: the carrier of b, the carrier of b:] -defined the carrier of b -valued Function-like quasi_total Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]

the multF of p || the carrier of b is set

the multF of p | [: the carrier of b, the carrier of b:] is Relation-like set

the multF of b || the carrier of a is set

the multF of b | [: the carrier of a, the carrier of a:] is Relation-like set

the multF of p || the carrier of a is set

the multF of p | [: the carrier of a, the carrier of a:] is Relation-like set

the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

1. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the OneF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

1. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the OneF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

0. a is V61(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

0. p is V61(p) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

the ZeroF of p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of p

1. b is V61(b) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

the OneF of b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

0. b is V61(b) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

the ZeroF of b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of b

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

b is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

L is set

the carrier of a is non empty non trivial set

the carrier of b is non empty non trivial set

L is set

F is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

b is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

the carrier of a is non empty non trivial set

the carrier of b is non empty non trivial set

p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

b is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

L is set

F is set

p is non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

p is non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

card p is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

the carrier of p is non empty non trivial finite set

card the carrier of p is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card the carrier of p is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal V113() V117() V118() V119() V120() V121() V122() Element of NAT

p is non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

(p) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal V113() V117() V118() V119() V120() V121() V122() Element of NAT

the carrier of p is non empty non trivial finite set

card the carrier of p is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

a is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (p)

card a is V4() V5() V6() cardinal set

the carrier of a is non empty non trivial set

card the carrier of a is non empty V4() V5() V6() cardinal set

p is non empty V4() V5() V6() V10() V11() V12() integer V14() ext-real positive non negative finite cardinal set

INT.Ring p is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

Segm p is V117() V118() V119() V120() V121() V122() Element of bool NAT

addint p is Relation-like [:(Segm p),(Segm p):] -defined Segm p -valued Function-like quasi_total V35() V36() V37() V38() Element of bool [:[:(Segm p),(Segm p):],(Segm p):]

[:(Segm p),(Segm p):] is RAT -valued INT -valued V35() V36() V37() V38() set

[:[:(Segm p),(Segm p):],(Segm p):] is RAT -valued INT -valued V35() V36() V37() V38() set

bool [:[:(Segm p),(Segm p):],(Segm p):] is non empty set

multint p is Relation-like [:(Segm p),(Segm p):] -defined Segm p -valued Function-like quasi_total V35() V36() V37() V38() Element of bool [:[:(Segm p),(Segm p):],(Segm p):]

K633(1,(Segm p)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal V113() Element of Segm p

K633(0,(Segm p)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal V113() Element of Segm p

doubleLoopStr(# (Segm p),(addint p),(multint p),K633(1,(Segm p)),K633(0,(Segm p)) #) is strict doubleLoopStr

p is non empty V4() V5() V6() V10() V11() V12() integer V14() ext-real positive non negative finite cardinal set

INT.Ring p is non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict unital associative commutative Euclidian right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

Segm p is V117() V118() V119() V120() V121() V122() Element of bool NAT

addint p is Relation-like [:(Segm p),(Segm p):] -defined Segm p -valued Function-like quasi_total V35() V36() V37() V38() Element of bool [:[:(Segm p),(Segm p):],(Segm p):]

[:(Segm p),(Segm p):] is RAT -valued INT -valued V35() V36() V37() V38() set

[:[:(Segm p),(