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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Element of NAT * : len b1 = 1 } is set
[: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),(