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

p is V11() V12() integer V32() ext-real Element of INT

M . (c

c

multreal . (c

c

p is V11() V12() integer V32() ext-real Element of INT

M . (c

multreal . (c

c

multint . (c

M is Relation-like INT -defined INT -valued Function-like V29( INT , INT ) V50() V51() V52() Element of K6(K7(INT,INT))

c

M . c

- c

compreal . c

c

M . c

compreal . c

- c

compint . c

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

P is V11() V12() integer ext-real set

M * c

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

p * P is V11() V12() integer V32() ext-real Element of INT

multint . (M,c

multreal . (M,c

M * c

M + c

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

p + P is V11() V12() integer V32() ext-real Element of INT

addint . (M,c

addreal . (M,c

M + c

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

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

the multF of () . (c

c

(1. ()) * c

the multF of () . ((1. ()),c

(1. ()) * c

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

p is V11() V12() integer V32() ext-real Element of the carrier of ()

p * c

the multF of () . (p,c

p * c

P is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the multF of () . (c

c

c

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the addF of () . (c

c

p + c

the addF of () . (p,c

p + c

c

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the addF of () . (c

c

P is V11() V12() integer V32() ext-real Element of the carrier of ()

(c

the addF of () . ((c

(c

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

the addF of () . (c

c

p is V11() V12() integer V32() ext-real Element of the carrier of ()

P is V11() V12() ext-real Element of REAL

c

addreal . (P,c

P + c

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

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

the addF of () . (c

c

c

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

the multF of () . (c

c

c

the multF of () . (c

c

c

the multF of () . (c

c

(c

the addF of () . ((c

(c

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

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the multF of () . (c

c

p * c

the multF of () . (p,c

p * c

c

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the multF of () . (c

c

P is V11() V12() integer V32() ext-real Element of the carrier of ()

(c

the multF of () . ((c

(c

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

the multF of () . (c

c

c

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

the multF of () . (c

c

c

p is V11() V12() integer ext-real set

- 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 + c

the addF of () . (P,c

P + c

- c

c

|.c

abs c

- c

- c

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

p is set

[p,c

(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

p is V11() V12() integer V32() ext-real Element of the carrier of ()

c

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

() . c

(c

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

absreal . 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 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

abs c

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

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

(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

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

(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

(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

(c

(c

the multF of () . ((c

(c

(c

((c

the addF of () . (((c

((c

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

() . 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

the carrier of c

K7( the carrier of c

K6(K7( the carrier of c

0. c

the ZeroF of c

p is Relation-like 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

1. c

the OneF of c

e is Element of the carrier of c

e * p is Element of the carrier of c

the multF of c

K7( the carrier of c

K7(K7( the carrier of c

K6(K7(K7( the carrier of c

the multF of c

P * e is Element of the carrier of c

the multF of c

(P * e) * p is Element of the carrier of c

the multF of c

((P * e) * p) + (0. c

the addF of c

the addF of c

P * (1. c

the multF of c

(P * (1. c

the addF of c

P + (0. c

the addF of c

e is Element of the carrier of c

e * p is Element of the carrier of c

the multF of c

K7( the carrier of c

K7(K7( the carrier of c

K6(K7(K7( the carrier of c

the multF of c

a is Element of the carrier of c

(e * p) + a is Element of the carrier of c

the addF of c

the addF 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

the carrier of c

K7( the carrier of c

K6(K7( the carrier of c

0. c

the ZeroF of c

c

the carrier of c

the Relation-like the carrier of c

P is Element of the carrier of c

0. c

the ZeroF of c

p is Element of the carrier of c

p * (0. c

the multF of c

K7( the carrier of c

K7(K7( the carrier of c

K6(K7(K7( the carrier of c

the multF of c

e is Element of the carrier of c

P is Element of the carrier of c

0. c

the ZeroF of c

p is Element of the carrier of c

{ b

1. c

the OneF of c

(1. c

the multF of c

K7( the carrier of c

K7(K7( the carrier of c

K6(K7(K7( the carrier of c

the multF of c

(0. c

the multF of c

((1. c

the addF of c

the addF of c

((1. c

the addF of c

the Relation-like the carrier of 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

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

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

a9 is Element of the carrier of c

the Relation-like the carrier of c

{ b

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

b9 is Element of the carrier of c

b9 * p is Element of the carrier of c

the multF of c

(t * P) + (b9 * p) is Element of the carrier of c

the addF of c

t is Element of the carrier of c

t * P is Element of the carrier of c

the multF of c

b9 is Element of the carrier of c

b9 * p is Element of the carrier of c

the multF of c

(t * P) + (b9 * p) is Element of the carrier of c

the addF 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 is Element of the carrier of c

(cc * a9) + cc is Element of the carrier of c

the addF of c

the Relation-like the carrier of c

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

t is Element of the carrier of c

t * p is Element of the carrier of c

the multF of c

(s * P) + (t * p) is Element of the carrier of c

the addF of c

s is Element of the carrier of c

s * P is Element of the carrier of c

the multF of c

t is Element of the carrier of c

t *