:: INT_3 semantic presentation

REAL is non zero V33() complex-membered ext-real-membered real-membered V66() set
NAT is non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non zero V33() complex-membered V66() set
RAT is non zero V33() complex-membered ext-real-membered real-membered rational-membered V66() set
INT is non zero V33() complex-membered ext-real-membered real-membered rational-membered integer-membered V66() set
K7(COMPLEX,COMPLEX) is V50() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V50() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V50() V51() V52() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V50() V51() V52() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is RAT -valued V50() V51() V52() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued V50() V51() V52() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued V50() V51() V52() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V50() V51() V52() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7(NAT,NAT),NAT)) is set
NAT is non zero V4() V5() V6() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
K6(NAT) is set
K6(NAT) is set
K408() is non empty strict Group-like associative commutative V128() multMagma
the carrier of K408() is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered set
1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K7(1,1) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V50() V51() V52() set
K6(K7(K7(1,1),REAL)) is set
2 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K7(2,2) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7(2,2),REAL) is V50() V51() V52() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V169() L15()
the carrier of (TOP-REAL 2) is set
0 is zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() set
0 is zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of NAT
K43(1) is V11() V12() integer ext-real non positive Element of REAL
absreal is Relation-like REAL -defined REAL -valued Function-like V29( REAL , REAL ) V50() V51() V52() Element of K6(K7(REAL,REAL))
addint is Relation-like K7(INT,INT) -defined INT -valued Function-like V29(K7(INT,INT), INT ) V50() V51() V52() Element of K6(K7(K7(INT,INT),INT))
addreal is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V29(K7(REAL,REAL), REAL ) V50() V51() V52() Element of K6(K7(K7(REAL,REAL),REAL))
compreal is Relation-like REAL -defined REAL -valued Function-like V29( REAL , REAL ) V50() V51() V52() Element of K6(K7(REAL,REAL))
multreal is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V29(K7(REAL,REAL), REAL ) V50() V51() V52() Element of K6(K7(K7(REAL,REAL),REAL))
compint is Relation-like INT -defined INT -valued Function-like V29( INT , INT ) V50() V51() V52() Element of K6(K7(INT,INT))
multint is Relation-like K7(INT,INT) -defined INT -valued Function-like V29(K7(INT,INT), INT ) V50() V51() V52() Element of K6(K7(K7(INT,INT),INT))
{0} is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
M is Relation-like K7(INT,INT) -defined INT -valued Function-like V29(K7(INT,INT), INT ) V50() V51() V52() Element of K6(K7(K7(INT,INT),INT))
c₂ is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of INT
M . (c₂,p) is V11() V12() integer V32() ext-real Element of INT
c₂ * p is V11() V12() integer V32() ext-real Element of INT
multreal . (c₂,p) is set
c₂ is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of INT
M . (c₂,p) is V11() V12() integer V32() ext-real Element of INT
multreal . (c₂,p) is set
c₂ * p is V11() V12() integer V32() ext-real Element of INT
multint . (c₂,p) is V11() V12() integer V32() ext-real Element of INT
M is Relation-like INT -defined INT -valued Function-like V29( INT , INT ) V50() V51() V52() Element of K6(K7(INT,INT))
c₂ is V11() V12() integer V32() ext-real Element of INT
M . c₂ is V11() V12() integer V32() ext-real Element of INT
- c₂ is V11() V12() integer V32() ext-real Element of INT
compreal . c₂ is V11() V12() ext-real set
c₂ is V11() V12() integer V32() ext-real Element of INT
M . c₂ is V11() V12() integer V32() ext-real Element of INT
compreal . c₂ is V11() V12() ext-real set
- c₂ is V11() V12() integer V32() ext-real Element of INT
compint . c₂ is V11() V12() integer V32() ext-real Element of INT
In (1,INT) is V11() V12() integer V32() ext-real Element of INT
In (0,INT) is V11() V12() integer V32() ext-real Element of INT
doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is strict doubleLoopStr
() is doubleLoopStr
the carrier of () is set
M is Element of the carrier of ()
M is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer ext-real set
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer ext-real set
M * c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () is Relation-like K7( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V29(K7( the carrier of (), the carrier of ()), the carrier of ()) V50() V51() V52() Element of K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ()))
K7( the carrier of (), the carrier of ()) is RAT -valued INT -valued V50() V51() V52() set
K7(K7( the carrier of (), the carrier of ()), the carrier of ()) is RAT -valued INT -valued V50() V51() V52() set
K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ())) is set
the multF of () . (M,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * P is V11() V12() integer V32() ext-real Element of INT
multint . (M,c₂) is set
multreal . (M,c₂) is set
M * c₂ is V11() V12() integer V32() ext-real Element of INT
M + c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () is Relation-like K7( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like V29(K7( the carrier of (), the carrier of ()), the carrier of ()) V50() V51() V52() Element of K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ()))
the addF of () . (M,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + P is V11() V12() integer V32() ext-real Element of INT
addint . (M,c₂) is set
addreal . (M,c₂) is set
M + c₂ is V11() V12() integer V32() ext-real Element of INT
0. () is V11() V12() integer V32() ext-real zero Element of the carrier of ()
the ZeroF of () is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
1. () is V11() V12() integer V32() ext-real Element of the carrier of ()
the OneF of () is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * (1. ()) is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,(1. ())) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * (1. ()) is V11() V12() integer V32() ext-real Element of INT
(1. ()) * c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . ((1. ()),c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
(1. ()) * c₂ is V11() V12() integer V32() ext-real Element of INT
1_ () is V11() V12() integer V32() ext-real Element of the carrier of ()
1. () is V11() V12() integer V32() ext-real Element of the carrier of ()
the OneF of () is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * c₂ is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * P is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * P is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + p is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + p is V11() V12() integer V32() ext-real Element of INT
p + c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (p,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + c₂ is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + p is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + p is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂ + p) + P is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((c₂ + p),P) is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂ + p) + P is V11() V12() integer V32() ext-real Element of INT
p + P is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (p,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + P is V11() V12() integer V32() ext-real Element of INT
c₂ + (p + P) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (c₂,(p + P)) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + (p + P) is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() ext-real Element of REAL
c₂ is V11() V12() ext-real Element of REAL
addreal . (P,c₂) is V11() V12() ext-real Element of REAL
P + c₂ is V11() V12() ext-real Element of REAL
p + (0. ()) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (p,(0. ())) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + (0. ()) is V11() V12() integer V32() ext-real Element of INT
addreal . (p,(0. ())) is set
addreal . (p,0) is set
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer ext-real set
- p is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + P is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (c₂,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ + P is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer V32() ext-real Element of the carrier of ()
p + P is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (p,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + P is V11() V12() integer V32() ext-real Element of INT
c₂ * (p + P) is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,(p + P)) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * (p + P) is V11() V12() integer V32() ext-real Element of INT
c₂ * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of INT
c₂ * P is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * P is V11() V12() integer V32() ext-real Element of INT
(c₂ * p) + (c₂ * P) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((c₂ * p),(c₂ * P)) is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂ * p) + (c₂ * P) is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
a is V11() V12() integer V32() ext-real Element of the carrier of ()
e + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (e,a) is V11() V12() integer V32() ext-real Element of the carrier of ()
e + a is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(e + a) * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . ((e + a),p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e + a) * p is V11() V12() integer V32() ext-real Element of INT
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
a * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of INT
(e * p) + (a * p) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),(a * p)) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + (a * p) is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of INT
p * c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * c₂ is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂ * p) * P is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . ((c₂ * p),P) is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂ * p) * P is V11() V12() integer V32() ext-real Element of INT
p * P is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,P) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * P is V11() V12() integer V32() ext-real Element of INT
c₂ * (p * P) is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,(p * P)) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * (p * P) is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ * p is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer ext-real set
- c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
- p is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
P + c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (P,c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
P + c₂ is V11() V12() integer V32() ext-real Element of INT
- c₂ is V11() V12() integer V32() ext-real Element of INT
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
|.c₂.| is V11() V12() ext-real set
abs c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
- c₂ is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer V32() ext-real Element of the carrier of ()
K7( the carrier of (),NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7( the carrier of (),NAT)) is set
proj1 absreal is set
absreal | INT is Relation-like Function-like V50() V51() V52() set
proj1 (absreal | INT) is set
proj2 (absreal | INT) is complex-membered ext-real-membered real-membered set
c₂ is set
p is set
[p,c₂] is V26() set
(absreal | INT) . p is V11() V12() ext-real set
P is V11() V12() integer ext-real set
(absreal | INT) . P is V11() V12() ext-real set
absreal . P is V11() V12() ext-real set
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- P is V11() V12() integer V32() ext-real Element of INT
c₂ is Relation-like the carrier of () -defined NAT -valued Function-like V29( the carrier of (), NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of (),NAT))
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
() is Relation-like the carrier of () -defined NAT -valued Function-like V29( the carrier of (), NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of (),NAT))
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
() . c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂) is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer ext-real set
absreal . p is V11() V12() ext-real set
abs p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is V11() V12() integer ext-real set
absreal . c₂ is V11() V12() ext-real set
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real Element of REAL
abs p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- 1 is V11() V12() integer V32() ext-real non positive Element of INT
- (- 1) is V11() V12() integer V32() ext-real non negative Element of INT
- c₂ is V11() V12() integer V32() ext-real Element of INT
abs c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 * p is V11() V12() integer V32() ext-real Element of INT
e - (0 * p) is V11() V12() integer V32() ext-real Element of INT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 - 1 is V11() V12() integer V32() ext-real Element of INT
p - 1 is V11() V12() integer V32() ext-real Element of INT
- P is V11() V12() integer V32() ext-real Element of INT
P * p is V11() V12() integer V32() ext-real Element of INT
P - (P * p) is V11() V12() integer V32() ext-real Element of INT
(- P) * (p - 1) is V11() V12() integer V32() ext-real Element of INT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a9 is V11() V12() integer ext-real set
a9 * p is V11() V12() integer V32() ext-real Element of INT
P - (a9 * p) is V11() V12() integer V32() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
e - p is V11() V12() integer V32() ext-real Element of INT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e + t is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- t is V11() V12() integer V32() ext-real non positive Element of INT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a + 1 is V11() V12() integer V32() ext-real Element of INT
(a + 1) * p is V11() V12() integer V32() ext-real Element of INT
P - ((a + 1) * p) is V11() V12() integer V32() ext-real Element of INT
s is V11() V12() integer ext-real set
s * p is V11() V12() integer V32() ext-real Element of INT
P - (s * p) is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
() . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . a9 is V11() V12() ext-real set
abs e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . a2 is V11() V12() ext-real Element of REAL
abs a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
a9 + (a9 * p) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (a9,(a9 * p)) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 + (a9 * p) is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 * p is V11() V12() integer V32() ext-real Element of INT
e - (0 * p) is V11() V12() integer V32() ext-real Element of INT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 - 1 is V11() V12() integer V32() ext-real Element of INT
p - 1 is V11() V12() integer V32() ext-real Element of INT
- P is V11() V12() integer V32() ext-real Element of INT
P * p is V11() V12() integer V32() ext-real Element of INT
P - (P * p) is V11() V12() integer V32() ext-real Element of INT
(- P) * (p - 1) is V11() V12() integer V32() ext-real Element of INT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a9 is V11() V12() integer ext-real set
a9 * p is V11() V12() integer V32() ext-real Element of INT
P - (a9 * p) is V11() V12() integer V32() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer ext-real set
a * p is V11() V12() integer V32() ext-real Element of INT
P - (a * p) is V11() V12() integer V32() ext-real Element of INT
e - p is V11() V12() integer V32() ext-real Element of INT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e + t is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- t is V11() V12() integer V32() ext-real non positive Element of INT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a + 1 is V11() V12() integer V32() ext-real Element of INT
(a + 1) * p is V11() V12() integer V32() ext-real Element of INT
P - ((a + 1) * p) is V11() V12() integer V32() ext-real Element of INT
s is V11() V12() integer ext-real set
s * p is V11() V12() integer V32() ext-real Element of INT
P - (s * p) is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . a2 is V11() V12() ext-real Element of REAL
abs a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
a9 + (a9 * p) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (a9,(a9 * p)) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 + (a9 * p) is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (P,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((P * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + e is V11() V12() integer V32() ext-real Element of INT
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + a is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer ext-real set
a9 is V11() V12() integer ext-real set
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
a2 is V11() V12() integer ext-real set
s is V11() V12() integer ext-real set
a2 - s is V11() V12() integer V32() ext-real Element of INT
t is V11() V12() integer ext-real set
(a2 - s) * t is V11() V12() integer V32() ext-real Element of INT
absreal . t is V11() V12() ext-real set
absreal . (a2 - s) is V11() V12() ext-real set
(absreal . (a2 - s)) * (absreal . t) is V11() V12() ext-real Element of REAL
- P is V11() V12() integer V32() ext-real Element of the carrier of ()
- P is V11() V12() integer V32() ext-real Element of INT
p + (- P) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (p,(- P)) is V11() V12() integer V32() ext-real Element of the carrier of ()
p + (- P) is V11() V12() integer V32() ext-real Element of INT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is V11() V12() integer ext-real set
absreal . b is V11() V12() ext-real set
b9 is V11() V12() integer V32() ext-real Element of the carrier of ()
() . b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc * cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- a9 is V11() V12() integer V32() ext-real Element of INT
a9 + (- a9) is V11() V12() integer V32() ext-real Element of INT
a9 + 0 is V11() V12() integer V32() ext-real Element of INT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs ((a2 - s) * t) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs (a2 - s) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs t is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs (a2 - s)) * (abs t) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(absreal . (a2 - s)) * (abs t) is V11() V12() ext-real Element of REAL
a9 is V11() V12() integer ext-real set
a9 is V11() V12() integer ext-real set
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
- (a9 - a9) is V11() V12() integer V32() ext-real Element of INT
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
s is V11() V12() integer ext-real set
a2 is V11() V12() integer ext-real set
s - a2 is V11() V12() integer V32() ext-real Element of INT
t is V11() V12() integer ext-real set
(s - a2) * t is V11() V12() integer V32() ext-real Element of INT
absreal . t is V11() V12() ext-real set
absreal . (s - a2) is V11() V12() ext-real set
(absreal . (s - a2)) * (absreal . t) is V11() V12() ext-real Element of REAL
- p is V11() V12() integer V32() ext-real Element of the carrier of ()
- p is V11() V12() integer V32() ext-real Element of INT
P + (- p) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (P,(- p)) is V11() V12() integer V32() ext-real Element of the carrier of ()
P + (- p) is V11() V12() integer V32() ext-real Element of INT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is V11() V12() integer ext-real set
absreal . b is V11() V12() ext-real set
b9 is V11() V12() integer V32() ext-real Element of the carrier of ()
() . b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc * cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs ((s - a2) * t) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs (s - a2) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs t is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs (s - a2)) * (abs t) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(absreal . (s - a2)) * (abs t) is V11() V12() ext-real Element of REAL
- a9 is V11() V12() integer V32() ext-real Element of INT
a9 + (- a9) is V11() V12() integer V32() ext-real Element of INT
a9 + 0 is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer ext-real set
a9 is V11() V12() integer ext-real set
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer ext-real set
a9 is V11() V12() integer ext-real set
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
- P is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of INT
- e is V11() V12() integer V32() ext-real Element of the carrier of ()
- e is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
(a9 * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a9 * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of INT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs (- P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . P is V11() V12() ext-real set
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a * p),a9) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (P,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((P * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + e is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + a is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
P is V11() V12() integer ext-real set
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer ext-real set
- P is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of INT
- e is V11() V12() integer V32() ext-real Element of the carrier of ()
- e is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
(a9 * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a9 * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of INT
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs (- P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . P is V11() V12() ext-real set
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + p is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + p is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a9 * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + P is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),P) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + P is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + p is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a * p),p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + p is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂,p) * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . ((c₂,p),p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(c₂,p) * p is V11() V12() integer V32() ext-real Element of INT
(c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
((c₂,p) * p) + (c₂,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . (((c₂,p) * p),(c₂,p)) is V11() V12() integer V32() ext-real Element of the carrier of ()
((c₂,p) * p) + (c₂,p) is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (P,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
P * p is V11() V12() integer V32() ext-real Element of INT
(p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + p is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((P * p),p) is V11() V12() integer V32() ext-real Element of the carrier of ()
(P * p) + p is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
- P is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of INT
() . a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs (- P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . P is V11() V12() ext-real set
- e is V11() V12() integer V32() ext-real Element of the carrier of ()
- e is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
(a9 * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a9 * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of INT
() . e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a * p),a9) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of INT
() . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital doubleLoopStr
the carrier of c₂ is non zero set
K7( the carrier of c₂,NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7( the carrier of c₂,NAT)) is set
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of c₂,NAT))
p is Element of the carrier of c₂
P is Element of the carrier of c₂
p . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1. c₂ is Element of the carrier of c₂
the OneF of c₂ is Element of the carrier of c₂
e is Element of the carrier of c₂
e * p is Element of the carrier of c₂
the multF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
K7( the carrier of c₂, the carrier of c₂) is set
K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) is set
K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂)) is set
the multF of c₂ . (e,p) is Element of the carrier of c₂
P * e is Element of the carrier of c₂
the multF of c₂ . (P,e) is Element of the carrier of c₂
(P * e) * p is Element of the carrier of c₂
the multF of c₂ . ((P * e),p) is Element of the carrier of c₂
((P * e) * p) + (0. c₂) is Element of the carrier of c₂
the addF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
the addF of c₂ . (((P * e) * p),(0. c₂)) is Element of the carrier of c₂
P * (1. c₂) is Element of the carrier of c₂
the multF of c₂ . (P,(1. c₂)) is Element of the carrier of c₂
(P * (1. c₂)) + (0. c₂) is Element of the carrier of c₂
the addF of c₂ . ((P * (1. c₂)),(0. c₂)) is Element of the carrier of c₂
P + (0. c₂) is Element of the carrier of c₂
the addF of c₂ . (P,(0. c₂)) is Element of the carrier of c₂
e is Element of the carrier of c₂
e * p is Element of the carrier of c₂
the multF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
K7( the carrier of c₂, the carrier of c₂) is set
K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) is set
K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂)) is set
the multF of c₂ . (e,p) is Element of the carrier of c₂
a is Element of the carrier of c₂
(e * p) + a is Element of the carrier of c₂
the addF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
the addF of c₂ . ((e * p),a) is Element of the carrier of c₂
p . a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is Element of the carrier of c₂
P is Element of the carrier of c₂
p . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is non empty () doubleLoopStr
the carrier of c₂ is non zero set
K7( the carrier of c₂,NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7( the carrier of c₂,NAT)) is set
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
c₂ is non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like () doubleLoopStr
the carrier of c₂ is non zero V2() set
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) is Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂)
P is Element of the carrier of c₂
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
p * (0. c₂) is Element of the carrier of c₂
the multF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
K7( the carrier of c₂, the carrier of c₂) is set
K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) is set
K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂)) is set
the multF of c₂ . (p,(0. c₂)) is Element of the carrier of c₂
e is Element of the carrier of c₂
P is Element of the carrier of c₂
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
{ b₁ where b₁ is Element of the carrier of c₂ : ex b₂, b₃ being Element of the carrier of c₂ st b₁ = (b₂ * P) + (b₃ * p) } is set
1. c₂ is non zero Element of the carrier of c₂
the OneF of c₂ is Element of the carrier of c₂
(1. c₂) * P is Element of the carrier of c₂
the multF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
K7( the carrier of c₂, the carrier of c₂) is set
K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) is set
K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂)) is set
the multF of c₂ . ((1. c₂),P) is Element of the carrier of c₂
(0. c₂) * p is Element of the carrier of c₂
the multF of c₂ . ((0. c₂),p) is Element of the carrier of c₂
((1. c₂) * P) + ((0. c₂) * p) is Element of the carrier of c₂
the addF of c₂ is Relation-like K7( the carrier of c₂, the carrier of c₂) -defined the carrier of c₂ -valued Function-like V29(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂) Element of K6(K7(K7( the carrier of c₂, the carrier of c₂), the carrier of c₂))
the addF of c₂ . (((1. c₂) * P),((0. c₂) * p)) is Element of the carrier of c₂
((1. c₂) * P) + (0. c₂) is Element of the carrier of c₂
the addF of c₂ . (((1. c₂) * P),(0. c₂)) is Element of the carrier of c₂
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) . P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is Element of the carrier of c₂
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a9 is Element of the carrier of c₂
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is Element of the carrier of c₂
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{ b₁ where b₁ is Element of the carrier of c₂ : ex b₂ being Element of the carrier of c₂ st b₁ = b₂ * a9 } is set
a2 is set
s is Element of the carrier of c₂
t is Element of the carrier of c₂
t * P is Element of the carrier of c₂
the multF of c₂ . (t,P) is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * p is Element of the carrier of c₂
the multF of c₂ . (b9,p) is Element of the carrier of c₂
(t * P) + (b9 * p) is Element of the carrier of c₂
the addF of c₂ . ((t * P),(b9 * p)) is Element of the carrier of c₂
t is Element of the carrier of c₂
t * P is Element of the carrier of c₂
the multF of c₂ . (t,P) is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * p is Element of the carrier of c₂
the multF of c₂ . (b9,p) is Element of the carrier of c₂
(t * P) + (b9 * p) is Element of the carrier of c₂
the addF of c₂ . ((t * P),(b9 * p)) is Element of the carrier of c₂
b is Element of the carrier of c₂
cc is Element of the carrier of c₂
cc * a9 is Element of the carrier of c₂
the multF of c₂ . (cc,a9) is Element of the carrier of c₂
cc is Element of the carrier of c₂
(cc * a9) + cc is Element of the carrier of c₂
the addF of c₂ . ((cc * a9),cc) is Element of the carrier of c₂
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() (c₂) . cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
z1 is Element of the carrier of c₂
s is Element of the carrier of c₂
s * P is Element of the carrier of c₂
the multF of c₂ . (s,P) is Element of the carrier of c₂
t is Element of the carrier of c₂
t * p is Element of the carrier of c₂
the multF of c₂ . (t,p) is Element of the carrier of c₂
(s * P) + (t * p) is Element of the carrier of c₂
the addF of c₂ . ((s * P),(t * p)) is Element of the carrier of c₂
s is Element of the carrier of c₂
s * P is Element of the carrier of c₂
the multF of c₂ . (s,P) is Element of the carrier of c₂
t is Element of the carrier of c₂
t * p is Element of the carrier of c₂
the multF of c₂ . (t,p) is Element of the carrier of c₂
(s * P) + (t * p) is Element of the carrier of c₂
the addF of c₂ . ((s * P),(t * p)) is Element of the carrier of c₂
- (cc * a9) is Element of the carrier of c₂
b + (- (cc * a9)) is Element of the carrier of c₂
the addF of c₂ . (b,(- (cc * a9))) is Element of the carrier of c₂
(cc * a9) + (- (cc * a9)) is Element of the carrier of c₂
the addF of c₂ . ((cc * a9),(- (cc * a9))) is Element of the carrier of c₂
cc + ((cc * a9) + (- (cc * a9))) is Element of the carrier of c₂
the addF of c₂ . (cc,((cc * a9) + (- (cc * a9)))) is Element of the carrier of c₂
cc + (0. c₂) is Element of the carrier of c₂
the addF of c₂ . (cc,(0. c₂)) is Element of the carrier of c₂
cc * (s * P) is Element of the carrier of c₂
the multF of c₂ . (cc,(s * P)) is Element of the carrier of c₂
cc * (t * p) is Element of the carrier of c₂
the multF of c₂ . (cc,(t * p)) is Element of the carrier of c₂
(cc * (s * P)) + (cc * (t * p)) is Element of the carrier of c₂
the addF of c₂ . ((cc * (s * P)),(cc * (t * p))) is Element of the carrier of c₂
- ((cc * (s * P)) + (cc * (t * p))) is Element of the carrier of c₂
b + (- ((cc * (s * P)) + (cc * (t * p)))) is Element of the carrier of c₂
the addF of c₂ . (b,(- ((cc * (s * P)) + (cc * (t * p))))) is Element of the carrier of c₂
- (cc * (s * P)) is Element of the carrier of c₂
- (cc * (t * p)) is Element of the carrier of c₂
(- (cc * (s * P))) + (- (cc * (t * p))) is Element of the carrier of c₂
the addF of c₂ . ((- (cc * (s * P))),(- (cc * (t * p)))) is Element of the carrier of c₂
b + ((- (cc * (s * P))) + (- (cc * (t * p)))) is Element of the carrier of c₂
the addF of c₂ . (b,((- (cc * (s * P))) + (- (cc * (t * p))))) is Element of the carrier of c₂
((t * P) + (b9 * p)) + (- (cc * (s * P))) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + (b9 * p)),(- (cc * (s * P)))) is Element of the carrier of c₂
(((t * P) + (b9 * p)) + (- (cc * (s * P)))) + (- (cc * (t * p))) is Element of the carrier of c₂
the addF of c₂ . ((((t * P) + (b9 * p)) + (- (cc * (s * P)))),(- (cc * (t * p)))) is Element of the carrier of c₂
(t * P) + (- (cc * (s * P))) is Element of the carrier of c₂
the addF of c₂ . ((t * P),(- (cc * (s * P)))) is Element of the carrier of c₂
((t * P) + (- (cc * (s * P)))) + (b9 * p) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + (- (cc * (s * P)))),(b9 * p)) is Element of the carrier of c₂
(((t * P) + (- (cc * (s * P)))) + (b9 * p)) + (- (cc * (t * p))) is Element of the carrier of c₂
the addF of c₂ . ((((t * P) + (- (cc * (s * P)))) + (b9 * p)),(- (cc * (t * p)))) is Element of the carrier of c₂
(b9 * p) + (- (cc * (t * p))) is Element of the carrier of c₂
the addF of c₂ . ((b9 * p),(- (cc * (t * p)))) is Element of the carrier of c₂
((t * P) + (- (cc * (s * P)))) + ((b9 * p) + (- (cc * (t * p)))) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + (- (cc * (s * P)))),((b9 * p) + (- (cc * (t * p))))) is Element of the carrier of c₂
- cc is Element of the carrier of c₂
(- cc) * (s * P) is Element of the carrier of c₂
the multF of c₂ . ((- cc),(s * P)) is Element of the carrier of c₂
(t * P) + ((- cc) * (s * P)) is Element of the carrier of c₂
the addF of c₂ . ((t * P),((- cc) * (s * P))) is Element of the carrier of c₂
((t * P) + ((- cc) * (s * P))) + ((b9 * p) + (- (cc * (t * p)))) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + ((- cc) * (s * P))),((b9 * p) + (- (cc * (t * p))))) is Element of the carrier of c₂
(- cc) * (t * p) is Element of the carrier of c₂
the multF of c₂ . ((- cc),(t * p)) is Element of the carrier of c₂
(b9 * p) + ((- cc) * (t * p)) is Element of the carrier of c₂
the addF of c₂ . ((b9 * p),((- cc) * (t * p))) is Element of the carrier of c₂
((t * P) + ((- cc) * (s * P))) + ((b9 * p) + ((- cc) * (t * p))) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + ((- cc) * (s * P))),((b9 * p) + ((- cc) * (t * p)))) is Element of the carrier of c₂
(- cc) * s is Element of the carrier of c₂
the multF of c₂ . ((- cc),s) is Element of the carrier of c₂
((- cc) * s) * P is Element of the carrier of c₂
the multF of c₂ . (((- cc) * s),P) is Element of the carrier of c₂
(t * P) + (((- cc) * s) * P) is Element of the carrier of c₂
the addF of c₂ . ((t * P),(((- cc) * s) * P)) is Element of the carrier of c₂
((t * P) + (((- cc) * s) * P)) + ((b9 * p) + ((- cc) * (t * p))) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + (((- cc) * s) * P)),((b9 * p) + ((- cc) * (t * p)))) is Element of the carrier of c₂
(- cc) * t is Element of the carrier of c₂
the multF of c₂ . ((- cc),t) is Element of the carrier of c₂
((- cc) * t) * p is Element of the carrier of c₂
the multF of c₂ . (((- cc) * t),p) is Element of the carrier of c₂
(b9 * p) + (((- cc) * t) * p) is Element of the carrier of c₂
the addF of c₂ . ((b9 * p),(((- cc) * t) * p)) is Element of the carrier of c₂
((t * P) + (((- cc) * s) * P)) + ((b9 * p) + (((- cc) * t) * p)) is Element of the carrier of c₂
the addF of c₂ . (((t * P) + (((- cc) * s) * P)),((b9 * p) + (((- cc) * t) * p))) is Element of the carrier of c₂
t + ((- cc) * s) is Element of the carrier of c₂
the addF of c₂ . (t,((- cc) * s)) is Element of the carrier of c₂
(t + ((- cc) * s)) * P is Element of the carrier of c₂
the multF of c₂ . ((t + ((- cc) * s)),P) is Element of the carrier of c₂
((t + ((- cc) * s)) * P) + ((b9 * p) + (((- cc) * t) * p)) is Element of the carrier of c₂
the addF of c₂ . (((t + ((- cc) * s)) * P),((b9 * p) + (((- cc) * t) * p))) is Element of the carrier of c₂
b9 + ((- cc) * t) is Element of the carrier of c₂
the addF of c₂ . (b9,((- cc) * t)) is Element of the carrier of c₂
(b9 + ((- cc) * t)) * p is Element of the carrier of c₂
the multF of c₂ . ((b9 + ((- cc) * t)),p) is Element of the carrier of c₂
((t + ((- cc) * s)) * P) + ((b9 + ((- cc) * t)) * p) is Element of the carrier of c₂
the addF of c₂ . (((t + ((- cc) * s)) * P),((b9 + ((- cc) * t)) * p)) is Element of the carrier of c₂
a2 is Element of the carrier of c₂
s is Element of the carrier of c₂
a2 * s is Element of the carrier of c₂
the multF of c₂ . (a2,s) is Element of the carrier of c₂
t is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * P is Element of the carrier of c₂
the multF of c₂ . (b9,P) is Element of the carrier of c₂
b is Element of the carrier of c₂
b * p is Element of the carrier of c₂
the multF of c₂ . (b,p) is Element of the carrier of c₂
(b9 * P) + (b * p) is Element of the carrier of c₂
the addF of c₂ . ((b9 * P),(b * p)) is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * P is Element of the carrier of c₂
the multF of c₂ . (b9,P) is Element of the carrier of c₂
b is Element of the carrier of c₂
b * p is Element of the carrier of c₂
the multF of c₂ . (b,p) is Element of the carrier of c₂
(b9 * P) + (b * p) is Element of the carrier of c₂
the addF of c₂ . ((b9 * P),(b * p)) is Element of the carrier of c₂
cc is Element of the carrier of c₂
a2 * cc is Element of the carrier of c₂
the multF of c₂ . (a2,cc) is Element of the carrier of c₂
b9 * s is Element of the carrier of c₂
the multF of c₂ . (b9,s) is Element of the carrier of c₂
(b9 * s) * a2 is Element of the carrier of c₂
the multF of c₂ . ((b9 * s),a2) is Element of the carrier of c₂
cc * a2 is Element of the carrier of c₂
the multF of c₂ . (cc,a2) is Element of the carrier of c₂
b * (cc * a2) is Element of the carrier of c₂
the multF of c₂ . (b,(cc * a2)) is Element of the carrier of c₂
((b9 * s) * a2) + (b * (cc * a2)) is Element of the carrier of c₂
the addF of c₂ . (((b9 * s) * a2),(b * (cc * a2))) is Element of the carrier of c₂
b * cc is Element of the carrier of c₂
the multF of c₂ . (b,cc) is Element of the carrier of c₂
(b * cc) * a2 is Element of the carrier of c₂
the multF of c₂ . ((b * cc),a2) is Element of the carrier of c₂
((b9 * s) * a2) + ((b * cc) * a2) is Element of the carrier of c₂
the addF of c₂ . (((b9 * s) * a2),((b * cc) * a2)) is Element of the carrier of c₂
(b9 * s) + (b * cc) is Element of the carrier of c₂
the addF of c₂ . ((b9 * s),(b * cc)) is Element of the carrier of c₂
((b9 * s) + (b * cc)) * a2 is Element of the carrier of c₂
the multF of c₂ . (((b9 * s) + (b * cc)),a2) is Element of the carrier of c₂
(0. c₂) * P is Element of the carrier of c₂
the multF of c₂ . ((0. c₂),P) is Element of the carrier of c₂
(1. c₂) * p is Element of the carrier of c₂
the multF of c₂ . ((1. c₂),p) is Element of the carrier of c₂
((0. c₂) * P) + ((1. c₂) * p) is Element of the carrier of c₂
the addF of c₂ . (((0. c₂) * P),((1. c₂) * p)) is Element of the carrier of c₂
(0. c₂) + ((1. c₂) * p) is Element of the carrier of c₂
the addF of c₂ . ((0. c₂),((1. c₂) * p)) is Element of the carrier of c₂
a2 is set
s is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * a9 is Element of the carrier of c₂
the multF of c₂ . (b9,a9) is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * a9 is Element of the carrier of c₂
the multF of c₂ . (b9,a9) is Element of the carrier of c₂
b is Element of the carrier of c₂
cc is Element of the carrier of c₂
cc * P is Element of the carrier of c₂
the multF of c₂ . (cc,P) is Element of the carrier of c₂
cc is Element of the carrier of c₂
cc * p is Element of the carrier of c₂
the multF of c₂ . (cc,p) is Element of the carrier of c₂
(cc * P) + (cc * p) is Element of the carrier of c₂
the addF of c₂ . ((cc * P),(cc * p)) is Element of the carrier of c₂
cc is Element of the carrier of c₂
cc * P is Element of the carrier of c₂
the multF of c₂ . (cc,P) is Element of the carrier of c₂
cc is Element of the carrier of c₂
cc * p is Element of the carrier of c₂
the multF of c₂ . (cc,p) is Element of the carrier of c₂
(cc * P) + (cc * p) is Element of the carrier of c₂
the addF of c₂ . ((cc * P),(cc * p)) is Element of the carrier of c₂
t is Element of the carrier of c₂
b9 * (cc * P) is Element of the carrier of c₂
the multF of c₂ . (b9,(cc * P)) is Element of the carrier of c₂
b9 * (cc * p) is Element of the carrier of c₂
the multF of c₂ . (b9,(cc * p)) is Element of the carrier of c₂
(b9 * (cc * P)) + (b9 * (cc * p)) is Element of the carrier of c₂
the addF of c₂ . ((b9 * (cc * P)),(b9 * (cc * p))) is Element of the carrier of c₂
b9 * cc is Element of the carrier of c₂
the multF of c₂ . (b9,cc) is Element of the carrier of c₂
(b9 * cc) * P is Element of the carrier of c₂
the multF of c₂ . ((b9 * cc),P) is Element of the carrier of c₂
((b9 * cc) * P) + (b9 * (cc * p)) is Element of the carrier of c₂
the addF of c₂ . (((b9 * cc) * P),(b9 * (cc * p))) is Element of the carrier of c₂
b9 * cc is Element of the carrier of c₂
the multF of c₂ . (b9,cc) is Element of the carrier of c₂
(b9 * cc) * p is Element of the carrier of c₂
the multF of c₂ . ((b9 * cc),p) is Element of the carrier of c₂
((b9 * cc) * P) + ((b9 * cc) * p) is Element of the carrier of c₂
the addF of c₂ . (((b9 * cc) * P),((b9 * cc) * p)) is Element of the carrier of c₂
a2 is Element of the carrier of c₂
s is Element of the carrier of c₂
s * a9 is Element of the carrier of c₂
the multF of c₂ . (s,a9) is Element of the carrier of c₂
t is Element of the carrier of c₂
b9 is Element of the carrier of c₂
b9 * a9 is Element of the carrier of c₂
the multF of c₂ . (b9,a9) is Element of the carrier of c₂
P is Element of the carrier of c₂
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
P is Element of the carrier of c₂
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
e is Element of the carrier of c₂
a is Element of the carrier of c₂
c₂ is non empty non degenerated V77() right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like doubleLoopStr
p is V11() V12() integer V32() ext-real Element of the carrier of ()
c₂ is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
- P is V11() V12() integer V32() ext-real Element of INT
p is V11() V12() integer V32() ext-real Element of the carrier of ()
() . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (e,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
e * p is V11() V12() integer V32() ext-real Element of INT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((e * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(e * p) + a is V11() V12() integer V32() ext-real Element of INT
() . a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . p is V11() V12() ext-real set
abs (- P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
absreal . P is V11() V12() ext-real set
- e is V11() V12() integer V32() ext-real Element of the carrier of ()
- e is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a9,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a9 * p is V11() V12() integer V32() ext-real Element of INT
(a9 * p) + a is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a9 * p),a) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a9 * p) + a is V11() V12() integer V32() ext-real Element of INT
P is V11() V12() integer ext-real set
P is V11() V12() integer ext-real set
p is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (p,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
p * p is V11() V12() integer V32() ext-real Element of INT
e is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((p * p),e) is V11() V12() integer V32() ext-real Element of the carrier of ()
(p * p) + e is V11() V12() integer V32() ext-real Element of INT
() . e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of the carrier of ()
the multF of () . (a,p) is V11() V12() integer V32() ext-real Element of the carrier of ()
a * p is V11() V12() integer V32() ext-real Element of INT
a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of the carrier of ()
the addF of () . ((a * p),a9) is V11() V12() integer V32() ext-real Element of the carrier of ()
(a * p) + a9 is V11() V12() integer V32() ext-real Element of INT
() . a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital doubleLoopStr
the carrier of c₂ is non zero set
K7( the carrier of c₂,NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7( the carrier of c₂,NAT)) is set
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of c₂,NAT)) is Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of c₂,NAT))
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
P is Element of the carrier of c₂
the Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of c₂,NAT)) . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is non empty doubleLoopStr
c₂ is non empty almost_left_invertible unital associative commutative right_zeroed right_unital well-unital left_unital () doubleLoopStr
the carrier of c₂ is non zero set
K7( the carrier of c₂,NAT) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7( the carrier of c₂,NAT)) is set
p is Relation-like the carrier of c₂ -defined NAT -valued Function-like V29( the carrier of c₂, NAT ) V50() V51() V52() V53() Element of K6(K7( the carrier of c₂,NAT))
0. c₂ is zero Element of the carrier of c₂
the ZeroF of c₂ is Element of the carrier of c₂
p is Element of the carrier of c₂
P is Element of the carrier of c₂
p . p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
P * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P * p) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e * a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(e * a) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
P is Relation-like K7((Segm p),(Segm p)) -defined Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
P is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
p is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7((Segm c₂),(Segm c₂))) is set
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
{ [b₁,((p - b₁) mod p)] where b₁ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : not p <= b₁ } is set
p is set
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - e is V11() V12() integer V32() ext-real Element of INT
(p - e) mod p is V11() V12() integer ext-real set
[e,((p - e) mod p)] is V26() set
p is set
e is set
[p,e] is V26() set
a is set
[p,a] is V26() set
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a9 is V11() V12() integer V32() ext-real Element of INT
(p - a9) mod p is V11() V12() integer ext-real set
[a9,((p - a9) mod p)] is V26() set
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a9 is V11() V12() integer V32() ext-real Element of INT
(p - a9) mod p is V11() V12() integer ext-real set
[a9,((p - a9) mod p)] is V26() set
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
p is Relation-like Function-like set
proj1 p is set
e is set
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a is V11() V12() integer V32() ext-real Element of INT
(p - a) mod p is V11() V12() integer ext-real set
[a,((p - a) mod p)] is V26() set
e is set
a is set
[e,a] is V26() set
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a9 is V11() V12() integer V32() ext-real Element of INT
(p - a9) mod p is V11() V12() integer ext-real set
[a9,((p - a9) mod p)] is V26() set
proj2 p is set
e is set
a is set
[a,e] is V26() set
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a9 is V11() V12() integer V32() ext-real Element of INT
(p - a9) mod p is V11() V12() integer ext-real set
[a9,((p - a9) mod p)] is V26() set
a9 - a9 is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7((Segm p),(Segm p))) is set
e is Relation-like Segm p -defined Segm p -valued Function-like V29( Segm p, Segm p) V50() V51() V52() V53() Element of K6(K7((Segm p),(Segm p)))
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
e . a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
p - a is V11() V12() integer V32() ext-real Element of INT
(p - a) mod p is V11() V12() integer ext-real set
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a9 is V11() V12() integer V32() ext-real Element of INT
(p - a9) mod p is V11() V12() integer ext-real set
[a9,((p - a9) mod p)] is V26() set
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7((Segm p),(Segm p))) is set
P is Relation-like Segm c₂ -defined Segm c₂ -valued Function-like V29( Segm c₂, Segm c₂) V50() V51() V52() V53() Element of K6(K7((Segm c₂),(Segm c₂)))
p is Relation-like Segm c₂ -defined Segm c₂ -valued Function-like V29( Segm c₂, Segm c₂) V50() V51() V52() V53() Element of K6(K7((Segm c₂),(Segm c₂)))
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
p + P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint c₂) . (p,P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
(p + P) - c₂ is V11() V12() integer V32() ext-real Element of INT
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(p + P) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
p * a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * a) + e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p * 1 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * 1) + (p * 1) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p * 2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
addint p is Relation-like K7((Segm p),(Segm p)) -defined INT -valued Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
(addint p) . (p,P) is set
(p + P) - p is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
p * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * a9) + ((p + P) mod p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * p) + ((p + P) mod p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
c₂ div p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p * (c₂ div p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂ div p) + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((c₂ div p) + 1) * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂ div p) * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((c₂ div p) * p) + p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(p * (c₂ div p)) + p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(p * (c₂ div p)) + p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
p * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂) . (p,P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a * c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a + 1) * c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * P) - (a * c₂) is V11() V12() integer V32() ext-real Element of INT
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p * e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * e) mod c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
c₂ * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂ * a9) + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(a * c₂) + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a9 + s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s * c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s * c₂) + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * c₂) + ((s * c₂) + a2) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(1 * c₂) + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ * (a + 1) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂) . (p,e) is set
(p * e) - (a * c₂) is V11() V12() integer V32() ext-real Element of INT
0 + (a * c₂) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((p * e) - (a * c₂)) + (a * c₂) is V11() V12() integer V32() ext-real Element of INT
c₂ * a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p * e) - (c₂ * a) is V11() V12() integer V32() ext-real Element of INT
(a * c₂) + c₂ is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
c₂ * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₂ * a9) + ((p * e) - (c₂ * a)) is V11() V12() integer V32() ext-real Element of INT
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(c₂) is Relation-like Segm c₂ -defined Segm c₂ -valued Function-like V29( Segm c₂, Segm c₂) V50() V51() V52() V53() Element of K6(K7((Segm c₂),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7((Segm c₂),(Segm c₂))) is set
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
(c₂) . p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
c₂ - p is V11() V12() integer V32() ext-real Element of INT
P is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P - p is V11() V12() integer V32() ext-real Element of INT
p - p is V11() V12() integer V32() ext-real Element of INT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e mod P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P) is Relation-like Segm P -defined Segm P -valued Function-like V29( Segm P, Segm P) V50() V51() V52() V53() Element of K6(K7((Segm P),(Segm P)))
Segm P is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
K7((Segm P),(Segm P)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7((Segm P),(Segm P))) is set
(P) . p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
P + p is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P + p) - p is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 mod P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
P * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P * a9) + (a9 mod P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * P) + (a9 mod P) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
P * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P * a9) + a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P - p) + p is V11() V12() integer V32() ext-real Element of INT
P + p is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P * 2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P * 1 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(P * 1) + (P * 1) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P + a is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * P is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
c₂ is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(c₂) is doubleLoopStr
Segm c₂ is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
(1) is non empty strict doubleLoopStr
Segm 1 is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint 1 is Relation-like K7((Segm 1),(Segm 1)) -defined INT -valued Segm 1 -valued Function-like V29(K7((Segm 1),(Segm 1)), Segm 1) V50() V51() V52() V53() Element of K6(K7(K7((Segm 1),(Segm 1)),(Segm 1)))
K7((Segm 1),(Segm 1)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm 1),(Segm 1)),(Segm 1)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm 1),(Segm 1)),(Segm 1))) is set
(1) is Relation-like K7((Segm 1),(Segm 1)) -defined Segm 1 -valued Function-like V29(K7((Segm 1),(Segm 1)), Segm 1) V50() V51() V52() V53() Element of K6(K7(K7((Segm 1),(Segm 1)),(Segm 1)))
In (1,(Segm 1)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm 1
In (0,(Segm 1)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm 1
doubleLoopStr(# (Segm 1),(addint 1),(1),(In (1,(Segm 1))),(In (0,(Segm 1))) #) is strict doubleLoopStr
the carrier of (1) is non zero set
0. (1) is zero Element of the carrier of (1)
the ZeroF of (1) is Element of the carrier of (1)
1. (1) is Element of the carrier of (1)
the OneF of (1) is Element of the carrier of (1)
P is Element of the carrier of (1)
P is Element of the carrier of (1)
p is Element of the carrier of (1)
P + p is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (P,p) is Element of the carrier of (1)
p + P is Element of the carrier of (1)
the addF of (1) . (p,P) is Element of the carrier of (1)
P is Element of the carrier of (1)
P + (0. (1)) is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (P,(0. (1))) is Element of the carrier of (1)
P is Element of the carrier of (1)
p is Element of the carrier of (1)
P * p is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the multF of (1) . (P,p) is Element of the carrier of (1)
e is Element of the carrier of (1)
(P * p) * e is Element of the carrier of (1)
the multF of (1) . ((P * p),e) is Element of the carrier of (1)
p * e is Element of the carrier of (1)
the multF of (1) . (p,e) is Element of the carrier of (1)
P * (p * e) is Element of the carrier of (1)
the multF of (1) . (P,(p * e)) is Element of the carrier of (1)
P is Element of the carrier of (1)
- P is Element of the carrier of (1)
P + (- P) is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (P,(- P)) is Element of the carrier of (1)
P is Element of the carrier of (1)
- P is Element of the carrier of (1)
P + (- P) is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (P,(- P)) is Element of the carrier of (1)
P is Element of the carrier of (1)
p is Element of the carrier of (1)
P + p is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (P,p) is Element of the carrier of (1)
e is Element of the carrier of (1)
(P + p) + e is Element of the carrier of (1)
the addF of (1) . ((P + p),e) is Element of the carrier of (1)
p + e is Element of the carrier of (1)
the addF of (1) . (p,e) is Element of the carrier of (1)
P + (p + e) is Element of the carrier of (1)
the addF of (1) . (P,(p + e)) is Element of the carrier of (1)
P is Element of the carrier of (1)
(1. (1)) * P is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the multF of (1) . ((1. (1)),P) is Element of the carrier of (1)
P * (1. (1)) is Element of the carrier of (1)
the multF of (1) . (P,(1. (1))) is Element of the carrier of (1)
P is Element of the carrier of (1)
P * (1. (1)) is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the multF of (1) . (P,(1. (1))) is Element of the carrier of (1)
(1. (1)) * P is Element of the carrier of (1)
the multF of (1) . ((1. (1)),P) is Element of the carrier of (1)
P is Element of the carrier of (1)
p is Element of the carrier of (1)
P * p is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the multF of (1) . (P,p) is Element of the carrier of (1)
p * P is Element of the carrier of (1)
the multF of (1) . (p,P) is Element of the carrier of (1)
P is Element of the carrier of (1)
p is Element of the carrier of (1)
e is Element of the carrier of (1)
p + e is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (p,e) is Element of the carrier of (1)
P * (p + e) is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
the multF of (1) . (P,(p + e)) is Element of the carrier of (1)
P * p is Element of the carrier of (1)
the multF of (1) . (P,p) is Element of the carrier of (1)
P * e is Element of the carrier of (1)
the multF of (1) . (P,e) is Element of the carrier of (1)
(P * p) + (P * e) is Element of the carrier of (1)
the addF of (1) . ((P * p),(P * e)) is Element of the carrier of (1)
p is Element of the carrier of (1)
e is Element of the carrier of (1)
p + e is Element of the carrier of (1)
the addF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
K7( the carrier of (1), the carrier of (1)) is set
K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) is set
K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1))) is set
the addF of (1) . (p,e) is Element of the carrier of (1)
P is Element of the carrier of (1)
(p + e) * P is Element of the carrier of (1)
the multF of (1) is Relation-like K7( the carrier of (1), the carrier of (1)) -defined the carrier of (1) -valued Function-like V29(K7( the carrier of (1), the carrier of (1)), the carrier of (1)) Element of K6(K7(K7( the carrier of (1), the carrier of (1)), the carrier of (1)))
the multF of (1) . ((p + e),P) is Element of the carrier of (1)
p * P is Element of the carrier of (1)
the multF of (1) . (p,P) is Element of the carrier of (1)
e * P is Element of the carrier of (1)
the multF of (1) . (e,P) is Element of the carrier of (1)
(p * P) + (e * P) is Element of the carrier of (1)
the addF of (1) . ((p * P),(e * P)) is Element of the carrier of (1)
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
p is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Segm p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
p - c₂ is V11() V12() integer V32() ext-real Element of INT
p - 0 is V11() V12() integer V32() ext-real non negative Element of INT
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(c₂) is doubleLoopStr
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
1. (c₂) is Element of the carrier of (c₂)
the carrier of (c₂) is set
the OneF of (c₂) is Element of the carrier of (c₂)
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(c₂) is doubleLoopStr
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(p) is non empty strict doubleLoopStr
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint p is Relation-like K7((Segm p),(Segm p)) -defined INT -valued Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
(p) is Relation-like K7((Segm p),(Segm p)) -defined Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
In (1,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
In (0,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
doubleLoopStr(# (Segm p),(addint p),(p),(In (1,(Segm p))),(In (0,(Segm p))) #) is strict doubleLoopStr
1. (p) is Element of the carrier of (p)
the carrier of (p) is non zero set
the OneF of (p) is Element of the carrier of (p)
p is Element of the carrier of (p)
(1. (p)) * p is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the multF of (p) . ((1. (p)),p) is Element of the carrier of (p)
p * (1. (p)) is Element of the carrier of (p)
the multF of (p) . (p,(1. (p))) is Element of the carrier of (p)
0 + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(0 + 1) * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
1 * e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p) . (p,1) is set
0 * p is zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V32() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of NAT
e - (0 * p) is V11() V12() integer V32() ext-real non negative Element of INT
(p) . (1,p) is set
p is Element of the carrier of (p)
p * (1. (p)) is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the multF of (p) . (p,(1. (p))) is Element of the carrier of (p)
(1. (p)) * p is Element of the carrier of (p)
the multF of (p) . ((1. (p)),p) is Element of the carrier of (p)
p is Element of the carrier of (p)
e is Element of the carrier of (p)
p + e is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (p,e) is Element of the carrier of (p)
e + p is Element of the carrier of (p)
the addF of (p) . (e,p) is Element of the carrier of (p)
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint p) . (p,e) is set
(addint p) . (e,p) is set
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint p) . (p,e) is set
(a + a9) - p is V11() V12() integer V32() ext-real Element of INT
(addint p) . (e,p) is set
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint p) . (p,e) is set
(addint p) . (e,p) is set
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint p) . (p,e) is set
(addint p) . (e,p) is set
p is Element of the carrier of (p)
e is Element of the carrier of (p)
p * e is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the multF of (p) . (p,e) is Element of the carrier of (p)
a is Element of the carrier of (p)
(p * e) * a is Element of the carrier of (p)
the multF of (p) . ((p * e),a) is Element of the carrier of (p)
e * a is Element of the carrier of (p)
the multF of (p) . (e,a) is Element of the carrier of (p)
p * (e * a) is Element of the carrier of (p)
the multF of (p) . (p,(e * a)) is Element of the carrier of (p)
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V11() V12() integer ext-real set
t is V11() V12() integer ext-real set
a9 * a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * a2) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * ((a9 * a2) mod p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * ((a9 * a2) mod p)) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t mod p is V11() V12() integer ext-real set
b is V11() V12() integer ext-real set
b * cc is V11() V12() integer V32() ext-real Element of INT
(b * cc) mod p is V11() V12() integer ext-real set
(t mod p) * ((b * cc) mod p) is V11() V12() integer V32() ext-real Element of INT
((t mod p) * ((b * cc) mod p)) mod p is V11() V12() integer ext-real set
t * (b * cc) is V11() V12() integer V32() ext-real Element of INT
(t * (b * cc)) mod p is V11() V12() integer ext-real set
t * b is V11() V12() integer V32() ext-real Element of INT
(t * b) * cc is V11() V12() integer V32() ext-real Element of INT
((t * b) * cc) mod p is V11() V12() integer ext-real set
(t * b) mod p is V11() V12() integer ext-real set
cc mod p is V11() V12() integer ext-real set
((t * b) mod p) * (cc mod p) is V11() V12() integer V32() ext-real Element of INT
(((t * b) mod p) * (cc mod p)) mod p is V11() V12() integer ext-real set
a9 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a9 * a9) mod p) * a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((a9 * a9) mod p) * a2) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p) . (a9,((a9 * a2) mod p)) is set
(p) . (((a9 * a9) mod p),a2) is set
p is Element of the carrier of (p)
e is Element of the carrier of (p)
p * e is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the multF of (p) . (p,e) is Element of the carrier of (p)
e * p is Element of the carrier of (p)
the multF of (p) . (e,p) is Element of the carrier of (p)
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 + 1 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 + 1) * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p) . (a,a9) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
(a * a9) - (a9 * p) is V11() V12() integer V32() ext-real Element of INT
(p) . (a9,a) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
p is Element of the carrier of (p)
e is Element of the carrier of (p)
p + e is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (p,e) is Element of the carrier of (p)
a is Element of the carrier of (p)
(p + e) + a is Element of the carrier of (p)
the addF of (p) . ((p + e),a) is Element of the carrier of (p)
e + a is Element of the carrier of (p)
the addF of (p) . (e,a) is Element of the carrier of (p)
p + (e + a) is Element of the carrier of (p)
the addF of (p) . (p,(e + a)) is Element of the carrier of (p)
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cc is V11() V12() integer ext-real set
t is V11() V12() integer ext-real set
a9 + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 + a2) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 + ((a9 + a2) mod p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 + ((a9 + a2) mod p)) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t mod p is V11() V12() integer ext-real set
b is V11() V12() integer ext-real set
b + cc is V11() V12() integer V32() ext-real Element of INT
(b + cc) mod p is V11() V12() integer ext-real set
(t mod p) + ((b + cc) mod p) is V11() V12() integer V32() ext-real Element of INT
((t mod p) + ((b + cc) mod p)) mod p is V11() V12() integer ext-real set
t + (b + cc) is V11() V12() integer V32() ext-real Element of INT
(t + (b + cc)) mod p is V11() V12() integer ext-real set
t + b is V11() V12() integer V32() ext-real Element of INT
(t + b) + cc is V11() V12() integer V32() ext-real Element of INT
((t + b) + cc) mod p is V11() V12() integer ext-real set
(t + b) mod p is V11() V12() integer ext-real set
cc mod p is V11() V12() integer ext-real set
((t + b) mod p) + (cc mod p) is V11() V12() integer V32() ext-real Element of INT
(((t + b) mod p) + (cc mod p)) mod p is V11() V12() integer ext-real set
a9 + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 + a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a9 + a9) mod p) + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((a9 + a9) mod p) + a2) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(addint p) . (a9,((a9 + a2) mod p)) is set
(addint p) . (((a9 + a9) mod p),a2) is set
0. (p) is zero Element of the carrier of (p)
the ZeroF of (p) is Element of the carrier of (p)
p is Element of the carrier of (p)
p + (0. (p)) is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (p,(0. (p))) is Element of the carrier of (p)
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
e + 0 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p is Element of the carrier of (p)
e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p + (0. (p)) is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (p,(0. (p))) is Element of the carrier of (p)
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p - a is V11() V12() integer V32() ext-real Element of INT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is Element of the carrier of (p)
p + a9 is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (p,a9) is Element of the carrier of (p)
a + a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a + a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e is Element of the carrier of (p)
a is Element of the carrier of (p)
e + a is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (e,a) is Element of the carrier of (p)
p is Element of the carrier of (p)
(e + a) * p is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
the multF of (p) . ((e + a),p) is Element of the carrier of (p)
e * p is Element of the carrier of (p)
the multF of (p) . (e,p) is Element of the carrier of (p)
a * p is Element of the carrier of (p)
the multF of (p) . (a,p) is Element of the carrier of (p)
(e * p) + (a * p) is Element of the carrier of (p)
the addF of (p) . ((e * p),(a * p)) is Element of the carrier of (p)
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
s is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
cc is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t is V11() V12() integer ext-real set
a9 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a2 * a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a9 * a9) mod p) + ((a2 * a9) mod p) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((a9 * a9) mod p) + ((a2 * a9) mod p)) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is V11() V12() integer ext-real set
b * t is V11() V12() integer V32() ext-real Element of INT
cc is V11() V12() integer ext-real set
cc * t is V11() V12() integer V32() ext-real Element of INT
(b * t) + (cc * t) is V11() V12() integer V32() ext-real Element of INT
((b * t) + (cc * t)) mod p is V11() V12() integer ext-real set
b + cc is V11() V12() integer V32() ext-real Element of INT
(b + cc) * t is V11() V12() integer V32() ext-real Element of INT
((b + cc) * t) mod p is V11() V12() integer ext-real set
(b + cc) mod p is V11() V12() integer ext-real set
t mod p is V11() V12() integer ext-real set
((b + cc) mod p) * (t mod p) is V11() V12() integer V32() ext-real Element of INT
(((b + cc) mod p) * (t mod p)) mod p is V11() V12() integer ext-real set
a9 + a2 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 + a2) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a9 + a2) mod p) * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((a9 + a2) mod p) * a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(cc * t) mod p is V11() V12() integer ext-real set
(b * t) mod p is V11() V12() integer ext-real set
(p) . (((a9 + a2) mod p),a9) is set
(p) . (e,p) is set
(addint p) . (((p) . (e,p)),((a2 * a9) mod p)) is set
(addint p) . (((a9 * a9) mod p),((a2 * a9) mod p)) is set
p is Element of the carrier of (p)
e is Element of the carrier of (p)
a is Element of the carrier of (p)
e + a is Element of the carrier of (p)
the addF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the addF of (p) . (e,a) is Element of the carrier of (p)
p * (e + a) is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
the multF of (p) . (p,(e + a)) is Element of the carrier of (p)
p * e is Element of the carrier of (p)
the multF of (p) . (p,e) is Element of the carrier of (p)
p * a is Element of the carrier of (p)
the multF of (p) . (p,a) is Element of the carrier of (p)
(p * e) + (p * a) is Element of the carrier of (p)
the addF of (p) . ((p * e),(p * a)) is Element of the carrier of (p)
(e + a) * p is Element of the carrier of (p)
the multF of (p) . ((e + a),p) is Element of the carrier of (p)
e * p is Element of the carrier of (p)
the multF of (p) . (e,p) is Element of the carrier of (p)
a * p is Element of the carrier of (p)
the multF of (p) . (a,p) is Element of the carrier of (p)
(e * p) + (a * p) is Element of the carrier of (p)
the addF of (p) . ((e * p),(a * p)) is Element of the carrier of (p)
(p * e) + (a * p) is Element of the carrier of (p)
the addF of (p) . ((p * e),(a * p)) is Element of the carrier of (p)
p is non empty right_complementable unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(c₂) is doubleLoopStr
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
p is non zero V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(p) is non empty strict doubleLoopStr
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint p is Relation-like K7((Segm p),(Segm p)) -defined INT -valued Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
(p) is Relation-like K7((Segm p),(Segm p)) -defined Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
In (1,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
In (0,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
doubleLoopStr(# (Segm p),(addint p),(p),(In (1,(Segm p))),(In (0,(Segm p))) #) is strict doubleLoopStr
p is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(p) is non empty strict doubleLoopStr
Segm p is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint p is Relation-like K7((Segm p),(Segm p)) -defined INT -valued Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
K7((Segm p),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm p),(Segm p)),(Segm p)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm p),(Segm p)),(Segm p))) is set
(p) is Relation-like K7((Segm p),(Segm p)) -defined Segm p -valued Function-like V29(K7((Segm p),(Segm p)), Segm p) V50() V51() V52() V53() Element of K6(K7(K7((Segm p),(Segm p)),(Segm p)))
In (1,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
In (0,(Segm p)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
doubleLoopStr(# (Segm p),(addint p),(p),(In (1,(Segm p))),(In (0,(Segm p))) #) is strict doubleLoopStr
e is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
e * a is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
e * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
p * e is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0. (p) is zero Element of the carrier of (p)
the carrier of (p) is non zero set
the ZeroF of (p) is Element of the carrier of (p)
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a2 is Element of the carrier of (p)
s is Element of the carrier of (p)
a2 * s is Element of the carrier of (p)
the multF of (p) is Relation-like K7( the carrier of (p), the carrier of (p)) -defined the carrier of (p) -valued Function-like V29(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) Element of K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)))
K7( the carrier of (p), the carrier of (p)) is set
K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p)) is set
K6(K7(K7( the carrier of (p), the carrier of (p)), the carrier of (p))) is set
the multF of (p) . (a2,s) is Element of the carrier of (p)
a9 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * a9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
P is non empty right_complementable unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of P is non zero set
0. P is zero Element of the carrier of P
the ZeroF of P is Element of the carrier of P
1. P is Element of the carrier of P
the OneF of P is Element of the carrier of P
a is Element of the carrier of P
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
t is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
s * t is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non zero V4() V5() V6() V10() V11() V12() integer V32() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
t * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 * a9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a9 gcd p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is V11() V12() integer ext-real set
s * a9 is V11() V12() integer V32() ext-real Element of INT
t is V11() V12() integer ext-real set
t * p is V11() V12() integer V32() ext-real Element of INT
(s * a9) + (t * p) is V11() V12() integer V32() ext-real Element of INT
s mod p is V11() V12() integer ext-real set
b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm p
b is Element of the carrier of P
b * a is Element of the carrier of P
the multF of P is Relation-like K7( the carrier of P, the carrier of P) -defined the carrier of P -valued Function-like V29(K7( the carrier of P, the carrier of P), the carrier of P) Element of K6(K7(K7( the carrier of P, the carrier of P), the carrier of P))
K7( the carrier of P, the carrier of P) is set
K7(K7( the carrier of P, the carrier of P), the carrier of P) is set
K6(K7(K7( the carrier of P, the carrier of P), the carrier of P)) is set
the multF of P . (b,a) is Element of the carrier of P
a9 * b9 is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a9 * b9) mod p is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a2 is V11() V12() integer ext-real set
a2 mod p is V11() V12() integer ext-real set
(s mod p) mod p is V11() V12() integer ext-real set
(a2 mod p) * ((s mod p) mod p) is V11() V12() integer V32() ext-real Element of INT
((a2 mod p) * ((s mod p) mod p)) mod p is V11() V12() integer ext-real set
(a2 mod p) * (s mod p) is V11() V12() integer V32() ext-real Element of INT
((a2 mod p) * (s mod p)) mod p is V11() V12() integer ext-real set
a2 * s is V11() V12() integer V32() ext-real Element of INT
(a2 * s) mod p is V11() V12() integer ext-real set
e is V11() V12() integer ext-real set
e mod p is V11() V12() integer ext-real set
c₂ is V4() V5() V6() V10() V11() V12() integer prime ext-real non negative set
SetPrimenumber 2 is zero V4() V5() V6() V8() V9() V10() V11() V12() integer Function-like functional V33() ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() Element of K6(NAT)
c₂ is non zero V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative set
(c₂) is non empty strict doubleLoopStr
Segm c₂ is non zero complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
c₂ is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(c₂) is doubleLoopStr
Segm c₂ is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
addint c₂ is Relation-like K7((Segm c₂),(Segm c₂)) -defined INT -valued Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
K7((Segm c₂),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)) is RAT -valued INT -valued V50() V51() V52() V53() set
K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂))) is set
(c₂) is Relation-like K7((Segm c₂),(Segm c₂)) -defined Segm c₂ -valued Function-like V29(K7((Segm c₂),(Segm c₂)), Segm c₂) V50() V51() V52() V53() Element of K6(K7(K7((Segm c₂),(Segm c₂)),(Segm c₂)))
In (1,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
In (0,(Segm c₂)) is V4() V5() V6() V10() V11() V12() integer V32() ext-real non negative Element of Segm c₂
doubleLoopStr(# (Segm c₂),(addint c₂),(c₂),(In (1,(Segm c₂))),(In (0,(Segm c₂))) #) is strict doubleLoopStr
1. (c₂) is Element of the carrier of (c₂)
the carrier of (c₂) is set
the OneF of (c₂) is Element of the carrier of (c₂)