REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
COMPLEX is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is non empty set
bool NAT is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
[:1,1:] is non empty V18() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V18() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is V18() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is V18() set
[:[:REAL,REAL:],REAL:] is V18() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
[:2,2:] is non empty V18() set
[:[:2,2:],REAL:] is V18() set
bool [:[:2,2:],REAL:] is non empty set
RAT is set
INT is set
bool [:REAL,REAL:] is non empty set
K340(2) is V159() L15()
the carrier of K340(2) is set
K414() is non empty non trivial V54() strict unital V170() right_unital well-unital left_unital doubleLoopStr
the carrier of K414() is non empty non trivial V36() V139() set
[: the carrier of K414(),NAT:] is non empty V18() set
bool [: the carrier of K414(),NAT:] is non empty set
[:COMPLEX,COMPLEX:] is V18() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V18() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is V18() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is V18() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is V18() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is V18() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty V18() set
[:[:NAT,NAT:],NAT:] is non empty V18() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer ext-real V18() non-empty empty-yielding set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer ext-real V18() non-empty empty-yielding Element of NAT
[:NAT,NAT,NAT:] is non empty set
[0,0,0] is V29() triple Element of [:NAT,NAT,NAT:]
K23(0,0) is V29() set
K23(K23(0,0),0) is V29() set
{[0,0,0]} is non empty Element of bool [:NAT,NAT,NAT:]
bool [:NAT,NAT,NAT:] is non empty set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
27 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real positive Element of NAT
[0,1,0] is V29() triple Element of [:NAT,NAT,NAT:]
K23(0,1) is V29() set
K23(K23(0,1),0) is V29() set
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
z |^ 2 is Element of the carrier of p
power p is V18() Function-like V32([: the carrier of p,NAT:], the carrier of p) Element of bool [:[: the carrier of p,NAT:], the carrier of p:]
[: the carrier of p,NAT:] is non empty V18() set
[:[: the carrier of p,NAT:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p,NAT:], the carrier of p:] is non empty set
(power p) . (z,2) is set
F is Element of the carrier of p
- F is Element of the carrier of p
F |^ 2 is Element of the carrier of p
(power p) . (F,2) is set
z * z is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (z,z) is Element of the carrier of p
F * F is Element of the carrier of p
the multF of p . (F,F) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
1. p is V55(p) Element of the carrier of p
the carrier of p is non empty non trivial set
(1. p) " is Element of the carrier of p
0. p is V55(p) Element of the carrier of p
((1. p) ") * (1. p) is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (((1. p) "),(1. p)) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
0. p is V55(p) Element of the carrier of p
z is Element of the carrier of p
z " is Element of the carrier of p
F is Element of the carrier of p
F " is Element of the carrier of p
Q is Element of the carrier of p
Q * (z ") is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (Q,(z ")) is Element of the carrier of p
Q * F is Element of the carrier of p
the multF of p . (Q,F) is Element of the carrier of p
R is Element of the carrier of p
R * (F ") is Element of the carrier of p
the multF of p . (R,(F ")) is Element of the carrier of p
z * R is Element of the carrier of p
the multF of p . (z,R) is Element of the carrier of p
(z ") * z is Element of the carrier of p
the multF of p . ((z "),z) is Element of the carrier of p
Q * ((z ") * z) is Element of the carrier of p
the multF of p . (Q,((z ") * z)) is Element of the carrier of p
(R * (F ")) * z is Element of the carrier of p
the multF of p . ((R * (F ")),z) is Element of the carrier of p
1. p is V55(p) Element of the carrier of p
Q * (1. p) is Element of the carrier of p
the multF of p . (Q,(1. p)) is Element of the carrier of p
R * z is Element of the carrier of p
the multF of p . (R,z) is Element of the carrier of p
(R * z) * (F ") is Element of the carrier of p
the multF of p . ((R * z),(F ")) is Element of the carrier of p
(F ") * F is Element of the carrier of p
the multF of p . ((F "),F) is Element of the carrier of p
(R * z) * ((F ") * F) is Element of the carrier of p
the multF of p . ((R * z),((F ") * F)) is Element of the carrier of p
(R * z) * (1. p) is Element of the carrier of p
the multF of p . ((R * z),(1. p)) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
0. p is V55(p) Element of the carrier of p
z is Element of the carrier of p
z " is Element of the carrier of p
F is Element of the carrier of p
F " is Element of the carrier of p
Q is Element of the carrier of p
Q * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (Q,F) is Element of the carrier of p
Q * (z ") is Element of the carrier of p
the multF of p . (Q,(z ")) is Element of the carrier of p
R is Element of the carrier of p
z * R is Element of the carrier of p
the multF of p . (z,R) is Element of the carrier of p
R * (F ") is Element of the carrier of p
the multF of p . (R,(F ")) is Element of the carrier of p
(z * R) * (F ") is Element of the carrier of p
the multF of p . ((z * R),(F ")) is Element of the carrier of p
(F ") * F is Element of the carrier of p
the multF of p . ((F "),F) is Element of the carrier of p
Q * ((F ") * F) is Element of the carrier of p
the multF of p . (Q,((F ") * F)) is Element of the carrier of p
1. p is V55(p) Element of the carrier of p
Q * (1. p) is Element of the carrier of p
the multF of p . (Q,(1. p)) is Element of the carrier of p
(R * (F ")) * z is Element of the carrier of p
the multF of p . ((R * (F ")),z) is Element of the carrier of p
(z ") * z is Element of the carrier of p
the multF of p . ((z "),z) is Element of the carrier of p
(R * (F ")) * ((z ") * z) is Element of the carrier of p
the multF of p . ((R * (F ")),((z ") * z)) is Element of the carrier of p
(R * (F ")) * (1. p) is Element of the carrier of p
the multF of p . ((R * (F ")),(1. p)) is Element of the carrier of p
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real set
z is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of z is non empty non trivial set
0. z is V55(z) Element of the carrier of z
F is Element of the carrier of z
F |^ p is Element of the carrier of z
power z is V18() Function-like V32([: the carrier of z,NAT:], the carrier of z) Element of bool [:[: the carrier of z,NAT:], the carrier of z:]
[: the carrier of z,NAT:] is non empty V18() set
[:[: the carrier of z,NAT:], the carrier of z:] is non empty V18() set
bool [:[: the carrier of z,NAT:], the carrier of z:] is non empty set
(power z) . (F,p) is set
p - 1 is V11() V12() integer ext-real set
Q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real set
Q + 1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real Element of NAT
F |^ (Q + 1) is Element of the carrier of z
(power z) . (F,(Q + 1)) is set
F |^ Q is Element of the carrier of z
(power z) . (F,Q) is set
(F |^ Q) * F is Element of the carrier of z
the multF of z is V18() Function-like V32([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty V18() set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty V18() set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the multF of z . ((F |^ Q),F) is Element of the carrier of z
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
- z is Element of the carrier of p
F is Element of the carrier of p
- F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
0. p is V55(p) Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z + F) + Q is Element of the carrier of p
the addF of p . ((z + F),Q) is Element of the carrier of p
R is Element of the carrier of p
((z + F) + Q) + R is Element of the carrier of p
the addF of p . (((z + F) + Q),R) is Element of the carrier of p
R + F is Element of the carrier of p
the addF of p . (R,F) is Element of the carrier of p
(R + F) + Q is Element of the carrier of p
the addF of p . ((R + F),Q) is Element of the carrier of p
((R + F) + Q) + z is Element of the carrier of p
the addF of p . (((R + F) + Q),z) is Element of the carrier of p
z + R is Element of the carrier of p
the addF of p . (z,R) is Element of the carrier of p
(z + R) + Q is Element of the carrier of p
the addF of p . ((z + R),Q) is Element of the carrier of p
((z + R) + Q) + F is Element of the carrier of p
the addF of p . (((z + R) + Q),F) is Element of the carrier of p
F + Q is Element of the carrier of p
the addF of p . (F,Q) is Element of the carrier of p
(F + Q) + z is Element of the carrier of p
the addF of p . ((F + Q),z) is Element of the carrier of p
((F + Q) + z) + R is Element of the carrier of p
the addF of p . (((F + Q) + z),R) is Element of the carrier of p
R + (F + Q) is Element of the carrier of p
the addF of p . (R,(F + Q)) is Element of the carrier of p
(R + (F + Q)) + z is Element of the carrier of p
the addF of p . ((R + (F + Q)),z) is Element of the carrier of p
z + Q is Element of the carrier of p
the addF of p . (z,Q) is Element of the carrier of p
(z + Q) + F is Element of the carrier of p
the addF of p . ((z + Q),F) is Element of the carrier of p
((z + Q) + F) + R is Element of the carrier of p
the addF of p . (((z + Q) + F),R) is Element of the carrier of p
(z + Q) + R is Element of the carrier of p
the addF of p . ((z + Q),R) is Element of the carrier of p
((z + Q) + R) + F is Element of the carrier of p
the addF of p . (((z + Q) + R),F) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z + F) + Q is Element of the carrier of p
the addF of p . ((z + F),Q) is Element of the carrier of p
F + Q is Element of the carrier of p
the addF of p . (F,Q) is Element of the carrier of p
R is Element of the carrier of p
((z + F) + Q) + R is Element of the carrier of p
the addF of p . (((z + F) + Q),R) is Element of the carrier of p
(F + Q) + R is Element of the carrier of p
the addF of p . ((F + Q),R) is Element of the carrier of p
z + ((F + Q) + R) is Element of the carrier of p
the addF of p . (z,((F + Q) + R)) is Element of the carrier of p
o2 is Element of the carrier of p
(((z + F) + Q) + R) + o2 is Element of the carrier of p
the addF of p . ((((z + F) + Q) + R),o2) is Element of the carrier of p
((F + Q) + R) + o2 is Element of the carrier of p
the addF of p . (((F + Q) + R),o2) is Element of the carrier of p
z + (((F + Q) + R) + o2) is Element of the carrier of p
the addF of p . (z,(((F + Q) + R) + o2)) is Element of the carrier of p
Q + R is Element of the carrier of p
the addF of p . (Q,R) is Element of the carrier of p
(z + F) + (Q + R) is Element of the carrier of p
the addF of p . ((z + F),(Q + R)) is Element of the carrier of p
F + (Q + R) is Element of the carrier of p
the addF of p . (F,(Q + R)) is Element of the carrier of p
z + (F + (Q + R)) is Element of the carrier of p
the addF of p . (z,(F + (Q + R))) is Element of the carrier of p
R + o2 is Element of the carrier of p
the addF of p . (R,o2) is Element of the carrier of p
((z + F) + Q) + (R + o2) is Element of the carrier of p
the addF of p . (((z + F) + Q),(R + o2)) is Element of the carrier of p
Q + (R + o2) is Element of the carrier of p
the addF of p . (Q,(R + o2)) is Element of the carrier of p
(z + F) + (Q + (R + o2)) is Element of the carrier of p
the addF of p . ((z + F),(Q + (R + o2))) is Element of the carrier of p
F + (Q + (R + o2)) is Element of the carrier of p
the addF of p . (F,(Q + (R + o2))) is Element of the carrier of p
z + (F + (Q + (R + o2))) is Element of the carrier of p
the addF of p . (z,(F + (Q + (R + o2)))) is Element of the carrier of p
(F + Q) + (R + o2) is Element of the carrier of p
the addF of p . ((F + Q),(R + o2)) is Element of the carrier of p
z + ((F + Q) + (R + o2)) is Element of the carrier of p
the addF of p . (z,((F + Q) + (R + o2))) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z + F) + Q is Element of the carrier of p
the addF of p . ((z + F),Q) is Element of the carrier of p
F + Q is Element of the carrier of p
the addF of p . (F,Q) is Element of the carrier of p
R is Element of the carrier of p
((z + F) + Q) + R is Element of the carrier of p
the addF of p . (((z + F) + Q),R) is Element of the carrier of p
(F + Q) + R is Element of the carrier of p
the addF of p . ((F + Q),R) is Element of the carrier of p
o2 is Element of the carrier of p
(((z + F) + Q) + R) + o2 is Element of the carrier of p
the addF of p . ((((z + F) + Q) + R),o2) is Element of the carrier of p
((F + Q) + R) + o2 is Element of the carrier of p
the addF of p . (((F + Q) + R),o2) is Element of the carrier of p
O is Element of the carrier of p
((((z + F) + Q) + R) + o2) + O is Element of the carrier of p
the addF of p . (((((z + F) + Q) + R) + o2),O) is Element of the carrier of p
(((F + Q) + R) + o2) + O is Element of the carrier of p
the addF of p . ((((F + Q) + R) + o2),O) is Element of the carrier of p
z + ((((F + Q) + R) + o2) + O) is Element of the carrier of p
the addF of p . (z,((((F + Q) + R) + o2) + O)) is Element of the carrier of p
o2 + O is Element of the carrier of p
the addF of p . (o2,O) is Element of the carrier of p
(((z + F) + Q) + R) + (o2 + O) is Element of the carrier of p
the addF of p . ((((z + F) + Q) + R),(o2 + O)) is Element of the carrier of p
((F + Q) + R) + (o2 + O) is Element of the carrier of p
the addF of p . (((F + Q) + R),(o2 + O)) is Element of the carrier of p
z + (((F + Q) + R) + (o2 + O)) is Element of the carrier of p
the addF of p . (z,(((F + Q) + R) + (o2 + O))) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z * F) * Q is Element of the carrier of p
the multF of p . ((z * F),Q) is Element of the carrier of p
R is Element of the carrier of p
((z * F) * Q) * R is Element of the carrier of p
the multF of p . (((z * F) * Q),R) is Element of the carrier of p
R * F is Element of the carrier of p
the multF of p . (R,F) is Element of the carrier of p
(R * F) * Q is Element of the carrier of p
the multF of p . ((R * F),Q) is Element of the carrier of p
((R * F) * Q) * z is Element of the carrier of p
the multF of p . (((R * F) * Q),z) is Element of the carrier of p
z * R is Element of the carrier of p
the multF of p . (z,R) is Element of the carrier of p
(z * R) * Q is Element of the carrier of p
the multF of p . ((z * R),Q) is Element of the carrier of p
((z * R) * Q) * F is Element of the carrier of p
the multF of p . (((z * R) * Q),F) is Element of the carrier of p
F * Q is Element of the carrier of p
the multF of p . (F,Q) is Element of the carrier of p
(F * Q) * z is Element of the carrier of p
the multF of p . ((F * Q),z) is Element of the carrier of p
((F * Q) * z) * R is Element of the carrier of p
the multF of p . (((F * Q) * z),R) is Element of the carrier of p
R * (F * Q) is Element of the carrier of p
the multF of p . (R,(F * Q)) is Element of the carrier of p
(R * (F * Q)) * z is Element of the carrier of p
the multF of p . ((R * (F * Q)),z) is Element of the carrier of p
z * Q is Element of the carrier of p
the multF of p . (z,Q) is Element of the carrier of p
(z * Q) * F is Element of the carrier of p
the multF of p . ((z * Q),F) is Element of the carrier of p
((z * Q) * F) * R is Element of the carrier of p
the multF of p . (((z * Q) * F),R) is Element of the carrier of p
(z * Q) * R is Element of the carrier of p
the multF of p . ((z * Q),R) is Element of the carrier of p
((z * Q) * R) * F is Element of the carrier of p
the multF of p . (((z * Q) * R),F) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z * F) * Q is Element of the carrier of p
the multF of p . ((z * F),Q) is Element of the carrier of p
F * Q is Element of the carrier of p
the multF of p . (F,Q) is Element of the carrier of p
R is Element of the carrier of p
((z * F) * Q) * R is Element of the carrier of p
the multF of p . (((z * F) * Q),R) is Element of the carrier of p
(F * Q) * R is Element of the carrier of p
the multF of p . ((F * Q),R) is Element of the carrier of p
z * ((F * Q) * R) is Element of the carrier of p
the multF of p . (z,((F * Q) * R)) is Element of the carrier of p
o2 is Element of the carrier of p
(((z * F) * Q) * R) * o2 is Element of the carrier of p
the multF of p . ((((z * F) * Q) * R),o2) is Element of the carrier of p
((F * Q) * R) * o2 is Element of the carrier of p
the multF of p . (((F * Q) * R),o2) is Element of the carrier of p
z * (((F * Q) * R) * o2) is Element of the carrier of p
the multF of p . (z,(((F * Q) * R) * o2)) is Element of the carrier of p
Q * R is Element of the carrier of p
the multF of p . (Q,R) is Element of the carrier of p
(z * F) * (Q * R) is Element of the carrier of p
the multF of p . ((z * F),(Q * R)) is Element of the carrier of p
F * (Q * R) is Element of the carrier of p
the multF of p . (F,(Q * R)) is Element of the carrier of p
z * (F * (Q * R)) is Element of the carrier of p
the multF of p . (z,(F * (Q * R))) is Element of the carrier of p
R * o2 is Element of the carrier of p
the multF of p . (R,o2) is Element of the carrier of p
((z * F) * Q) * (R * o2) is Element of the carrier of p
the multF of p . (((z * F) * Q),(R * o2)) is Element of the carrier of p
Q * (R * o2) is Element of the carrier of p
the multF of p . (Q,(R * o2)) is Element of the carrier of p
(z * F) * (Q * (R * o2)) is Element of the carrier of p
the multF of p . ((z * F),(Q * (R * o2))) is Element of the carrier of p
F * (Q * (R * o2)) is Element of the carrier of p
the multF of p . (F,(Q * (R * o2))) is Element of the carrier of p
z * (F * (Q * (R * o2))) is Element of the carrier of p
the multF of p . (z,(F * (Q * (R * o2)))) is Element of the carrier of p
(F * Q) * (R * o2) is Element of the carrier of p
the multF of p . ((F * Q),(R * o2)) is Element of the carrier of p
z * ((F * Q) * (R * o2)) is Element of the carrier of p
the multF of p . (z,((F * Q) * (R * o2))) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (z,F) is Element of the carrier of p
Q is Element of the carrier of p
(z * F) * Q is Element of the carrier of p
the multF of p . ((z * F),Q) is Element of the carrier of p
F * Q is Element of the carrier of p
the multF of p . (F,Q) is Element of the carrier of p
R is Element of the carrier of p
((z * F) * Q) * R is Element of the carrier of p
the multF of p . (((z * F) * Q),R) is Element of the carrier of p
(F * Q) * R is Element of the carrier of p
the multF of p . ((F * Q),R) is Element of the carrier of p
z * ((F * Q) * R) is Element of the carrier of p
the multF of p . (z,((F * Q) * R)) is Element of the carrier of p
o2 is Element of the carrier of p
(((z * F) * Q) * R) * o2 is Element of the carrier of p
the multF of p . ((((z * F) * Q) * R),o2) is Element of the carrier of p
((F * Q) * R) * o2 is Element of the carrier of p
the multF of p . (((F * Q) * R),o2) is Element of the carrier of p
(z * ((F * Q) * R)) * o2 is Element of the carrier of p
the multF of p . ((z * ((F * Q) * R)),o2) is Element of the carrier of p
O is Element of the carrier of p
((((z * F) * Q) * R) * o2) * O is Element of the carrier of p
the multF of p . (((((z * F) * Q) * R) * o2),O) is Element of the carrier of p
(((F * Q) * R) * o2) * O is Element of the carrier of p
the multF of p . ((((F * Q) * R) * o2),O) is Element of the carrier of p
z * ((((F * Q) * R) * o2) * O) is Element of the carrier of p
the multF of p . (z,((((F * Q) * R) * o2) * O)) is Element of the carrier of p
((z * ((F * Q) * R)) * o2) * O is Element of the carrier of p
the multF of p . (((z * ((F * Q) * R)) * o2),O) is Element of the carrier of p
o2 * O is Element of the carrier of p
the multF of p . (o2,O) is Element of the carrier of p
(((z * F) * Q) * R) * (o2 * O) is Element of the carrier of p
the multF of p . ((((z * F) * Q) * R),(o2 * O)) is Element of the carrier of p
((F * Q) * R) * (o2 * O) is Element of the carrier of p
the multF of p . (((F * Q) * R),(o2 * O)) is Element of the carrier of p
z * (((F * Q) * R) * (o2 * O)) is Element of the carrier of p
the multF of p . (z,(((F * Q) * R) * (o2 * O))) is Element of the carrier of p
(z * ((F * Q) * R)) * (o2 * O) is Element of the carrier of p
the multF of p . ((z * ((F * Q) * R)),(o2 * O)) is Element of the carrier of p
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real set
z is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of z is non empty non trivial set
F is Element of the carrier of z
F |^ p is Element of the carrier of z
power z is V18() Function-like V32([: the carrier of z,NAT:], the carrier of z) Element of bool [:[: the carrier of z,NAT:], the carrier of z:]
[: the carrier of z,NAT:] is non empty V18() set
[:[: the carrier of z,NAT:], the carrier of z:] is non empty V18() set
bool [:[: the carrier of z,NAT:], the carrier of z:] is non empty set
(power z) . (F,p) is set
Q is Element of the carrier of z
F * Q is Element of the carrier of z
the multF of z is V18() Function-like V32([: the carrier of z, the carrier of z:], the carrier of z) Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is non empty V18() set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty V18() set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the multF of z . (F,Q) is Element of the carrier of z
Q |^ p is Element of the carrier of z
(power z) . (Q,p) is set
(F |^ p) * (Q |^ p) is Element of the carrier of z
the multF of z . ((F |^ p),(Q |^ p)) is Element of the carrier of z
R is Element of the carrier of z
(F * Q) * R is Element of the carrier of z
the multF of z . ((F * Q),R) is Element of the carrier of z
((F * Q) * R) |^ p is Element of the carrier of z
(power z) . (((F * Q) * R),p) is set
R |^ p is Element of the carrier of z
(power z) . (R,p) is set
((F |^ p) * (Q |^ p)) * (R |^ p) is Element of the carrier of z
the multF of z . (((F |^ p) * (Q |^ p)),(R |^ p)) is Element of the carrier of z
(F * Q) |^ p is Element of the carrier of z
(power z) . ((F * Q),p) is set
((F * Q) |^ p) * (R |^ p) is Element of the carrier of z
the multF of z . (((F * Q) |^ p),(R |^ p)) is Element of the carrier of z
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
F is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . (z,F) is Element of the carrier of p
- F is Element of the carrier of p
- (z * F) is Element of the carrier of p
Q is Element of the carrier of p
F + Q is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
the addF of p . (F,Q) is Element of the carrier of p
z * Q is Element of the carrier of p
the multF of p . (z,Q) is Element of the carrier of p
(z * F) + (z * Q) is Element of the carrier of p
the addF of p . ((z * F),(z * Q)) is Element of the carrier of p
F - Q is Element of the carrier of p
- Q is Element of the carrier of p
F + (- Q) is Element of the carrier of p
the addF of p . (F,(- Q)) is Element of the carrier of p
(z * F) - (z * Q) is Element of the carrier of p
- (z * Q) is Element of the carrier of p
(z * F) + (- (z * Q)) is Element of the carrier of p
the addF of p . ((z * F),(- (z * Q))) is Element of the carrier of p
(- F) + Q is Element of the carrier of p
the addF of p . ((- F),Q) is Element of the carrier of p
(- (z * F)) + (z * Q) is Element of the carrier of p
the addF of p . ((- (z * F)),(z * Q)) is Element of the carrier of p
(- F) - Q is Element of the carrier of p
(- F) + (- Q) is Element of the carrier of p
the addF of p . ((- F),(- Q)) is Element of the carrier of p
(- (z * F)) - (z * Q) is Element of the carrier of p
(- (z * F)) + (- (z * Q)) is Element of the carrier of p
the addF of p . ((- (z * F)),(- (z * Q))) is Element of the carrier of p
R is Element of the carrier of p
(F + Q) + R is Element of the carrier of p
the addF of p . ((F + Q),R) is Element of the carrier of p
z * ((F + Q) + R) is Element of the carrier of p
the multF of p . (z,((F + Q) + R)) is Element of the carrier of p
z * R is Element of the carrier of p
the multF of p . (z,R) is Element of the carrier of p
((z * F) + (z * Q)) + (z * R) is Element of the carrier of p
the addF of p . (((z * F) + (z * Q)),(z * R)) is Element of the carrier of p
(F + Q) - R is Element of the carrier of p
- R is Element of the carrier of p
(F + Q) + (- R) is Element of the carrier of p
the addF of p . ((F + Q),(- R)) is Element of the carrier of p
z * ((F + Q) - R) is Element of the carrier of p
the multF of p . (z,((F + Q) - R)) is Element of the carrier of p
((z * F) + (z * Q)) - (z * R) is Element of the carrier of p
- (z * R) is Element of the carrier of p
((z * F) + (z * Q)) + (- (z * R)) is Element of the carrier of p
the addF of p . (((z * F) + (z * Q)),(- (z * R))) is Element of the carrier of p
(F - Q) + R is Element of the carrier of p
the addF of p . ((F - Q),R) is Element of the carrier of p
z * ((F - Q) + R) is Element of the carrier of p
the multF of p . (z,((F - Q) + R)) is Element of the carrier of p
((z * F) - (z * Q)) + (z * R) is Element of the carrier of p
the addF of p . (((z * F) - (z * Q)),(z * R)) is Element of the carrier of p
(F - Q) - R is Element of the carrier of p
(F - Q) + (- R) is Element of the carrier of p
the addF of p . ((F - Q),(- R)) is Element of the carrier of p
z * ((F - Q) - R) is Element of the carrier of p
the multF of p . (z,((F - Q) - R)) is Element of the carrier of p
((z * F) - (z * Q)) - (z * R) is Element of the carrier of p
((z * F) - (z * Q)) + (- (z * R)) is Element of the carrier of p
the addF of p . (((z * F) - (z * Q)),(- (z * R))) is Element of the carrier of p
((- F) + Q) + R is Element of the carrier of p
the addF of p . (((- F) + Q),R) is Element of the carrier of p
z * (((- F) + Q) + R) is Element of the carrier of p
the multF of p . (z,(((- F) + Q) + R)) is Element of the carrier of p
((- (z * F)) + (z * Q)) + (z * R) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * Q)),(z * R)) is Element of the carrier of p
((- F) + Q) - R is Element of the carrier of p
((- F) + Q) + (- R) is Element of the carrier of p
the addF of p . (((- F) + Q),(- R)) is Element of the carrier of p
z * (((- F) + Q) - R) is Element of the carrier of p
the multF of p . (z,(((- F) + Q) - R)) is Element of the carrier of p
((- (z * F)) + (z * Q)) - (z * R) is Element of the carrier of p
((- (z * F)) + (z * Q)) + (- (z * R)) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * Q)),(- (z * R))) is Element of the carrier of p
((- F) - Q) + R is Element of the carrier of p
the addF of p . (((- F) - Q),R) is Element of the carrier of p
z * (((- F) - Q) + R) is Element of the carrier of p
the multF of p . (z,(((- F) - Q) + R)) is Element of the carrier of p
((- (z * F)) - (z * Q)) + (z * R) is Element of the carrier of p
the addF of p . (((- (z * F)) - (z * Q)),(z * R)) is Element of the carrier of p
((- F) - Q) - R is Element of the carrier of p
((- F) - Q) + (- R) is Element of the carrier of p
the addF of p . (((- F) - Q),(- R)) is Element of the carrier of p
z * (((- F) - Q) - R) is Element of the carrier of p
the multF of p . (z,(((- F) - Q) - R)) is Element of the carrier of p
((- (z * F)) - (z * Q)) - (z * R) is Element of the carrier of p
((- (z * F)) - (z * Q)) + (- (z * R)) is Element of the carrier of p
the addF of p . (((- (z * F)) - (z * Q)),(- (z * R))) is Element of the carrier of p
z * (F + Q) is Element of the carrier of p
the multF of p . (z,(F + Q)) is Element of the carrier of p
(z * (F + Q)) + (z * R) is Element of the carrier of p
the addF of p . ((z * (F + Q)),(z * R)) is Element of the carrier of p
z * (- R) is Element of the carrier of p
the multF of p . (z,(- R)) is Element of the carrier of p
(z * (F + Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . ((z * (F + Q)),(z * (- R))) is Element of the carrier of p
((z * F) + (z * Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . (((z * F) + (z * Q)),(z * (- R))) is Element of the carrier of p
F + (- Q) is Element of the carrier of p
z * (F + (- Q)) is Element of the carrier of p
the multF of p . (z,(F + (- Q))) is Element of the carrier of p
(z * (F + (- Q))) + (z * R) is Element of the carrier of p
the addF of p . ((z * (F + (- Q))),(z * R)) is Element of the carrier of p
z * (- Q) is Element of the carrier of p
the multF of p . (z,(- Q)) is Element of the carrier of p
(z * F) + (z * (- Q)) is Element of the carrier of p
the addF of p . ((z * F),(z * (- Q))) is Element of the carrier of p
((z * F) + (z * (- Q))) + (z * R) is Element of the carrier of p
the addF of p . (((z * F) + (z * (- Q))),(z * R)) is Element of the carrier of p
(z * (F + (- Q))) + (z * (- R)) is Element of the carrier of p
the addF of p . ((z * (F + (- Q))),(z * (- R))) is Element of the carrier of p
((z * F) + (z * (- Q))) + (z * (- R)) is Element of the carrier of p
the addF of p . (((z * F) + (z * (- Q))),(z * (- R))) is Element of the carrier of p
((z * F) - (z * Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . (((z * F) - (z * Q)),(z * (- R))) is Element of the carrier of p
z * ((- F) + Q) is Element of the carrier of p
the multF of p . (z,((- F) + Q)) is Element of the carrier of p
(z * ((- F) + Q)) + (z * R) is Element of the carrier of p
the addF of p . ((z * ((- F) + Q)),(z * R)) is Element of the carrier of p
z * (- F) is Element of the carrier of p
the multF of p . (z,(- F)) is Element of the carrier of p
(z * (- F)) + (z * Q) is Element of the carrier of p
the addF of p . ((z * (- F)),(z * Q)) is Element of the carrier of p
((z * (- F)) + (z * Q)) + (z * R) is Element of the carrier of p
the addF of p . (((z * (- F)) + (z * Q)),(z * R)) is Element of the carrier of p
(z * ((- F) + Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . ((z * ((- F) + Q)),(z * (- R))) is Element of the carrier of p
((z * (- F)) + (z * Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . (((z * (- F)) + (z * Q)),(z * (- R))) is Element of the carrier of p
((- (z * F)) + (z * Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * Q)),(z * (- R))) is Element of the carrier of p
(- F) + (- Q) is Element of the carrier of p
z * ((- F) + (- Q)) is Element of the carrier of p
the multF of p . (z,((- F) + (- Q))) is Element of the carrier of p
(z * ((- F) + (- Q))) + (z * R) is Element of the carrier of p
the addF of p . ((z * ((- F) + (- Q))),(z * R)) is Element of the carrier of p
(z * (- F)) + (z * (- Q)) is Element of the carrier of p
the addF of p . ((z * (- F)),(z * (- Q))) is Element of the carrier of p
((z * (- F)) + (z * (- Q))) + (z * R) is Element of the carrier of p
the addF of p . (((z * (- F)) + (z * (- Q))),(z * R)) is Element of the carrier of p
(- (z * F)) + (z * (- Q)) is Element of the carrier of p
the addF of p . ((- (z * F)),(z * (- Q))) is Element of the carrier of p
((- (z * F)) + (z * (- Q))) + (z * R) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * (- Q))),(z * R)) is Element of the carrier of p
(z * ((- F) + (- Q))) + (z * (- R)) is Element of the carrier of p
the addF of p . ((z * ((- F) + (- Q))),(z * (- R))) is Element of the carrier of p
((z * (- F)) + (z * (- Q))) + (z * (- R)) is Element of the carrier of p
the addF of p . (((z * (- F)) + (z * (- Q))),(z * (- R))) is Element of the carrier of p
((- (z * F)) + (z * (- Q))) + (z * (- R)) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * (- Q))),(z * (- R))) is Element of the carrier of p
((- (z * F)) - (z * Q)) + (z * (- R)) is Element of the carrier of p
the addF of p . (((- (z * F)) - (z * Q)),(z * (- R))) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
z |^ 2 is Element of the carrier of p
power p is V18() Function-like V32([: the carrier of p,NAT:], the carrier of p) Element of bool [:[: the carrier of p,NAT:], the carrier of p:]
[: the carrier of p,NAT:] is non empty V18() set
[:[: the carrier of p,NAT:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p,NAT:], the carrier of p:] is non empty set
(power p) . (z,2) is set
F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
z - F is Element of the carrier of p
- F is Element of the carrier of p
z + (- F) is Element of the carrier of p
the addF of p . (z,(- F)) is Element of the carrier of p
(z + F) * (z - F) is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
the multF of p . ((z + F),(z - F)) is Element of the carrier of p
F |^ 2 is Element of the carrier of p
(power p) . (F,2) is set
(z |^ 2) - (F |^ 2) is Element of the carrier of p
- (F |^ 2) is Element of the carrier of p
(z |^ 2) + (- (F |^ 2)) is Element of the carrier of p
the addF of p . ((z |^ 2),(- (F |^ 2))) is Element of the carrier of p
z * (z - F) is Element of the carrier of p
the multF of p . (z,(z - F)) is Element of the carrier of p
F * (z - F) is Element of the carrier of p
the multF of p . (F,(z - F)) is Element of the carrier of p
(z * (z - F)) + (F * (z - F)) is Element of the carrier of p
the addF of p . ((z * (z - F)),(F * (z - F))) is Element of the carrier of p
z * z is Element of the carrier of p
the multF of p . (z,z) is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p . (z,F) is Element of the carrier of p
(z * z) - (z * F) is Element of the carrier of p
- (z * F) is Element of the carrier of p
(z * z) + (- (z * F)) is Element of the carrier of p
the addF of p . ((z * z),(- (z * F))) is Element of the carrier of p
((z * z) - (z * F)) + (F * (z - F)) is Element of the carrier of p
the addF of p . (((z * z) - (z * F)),(F * (z - F))) is Element of the carrier of p
(z |^ 2) - (z * F) is Element of the carrier of p
(z |^ 2) + (- (z * F)) is Element of the carrier of p
the addF of p . ((z |^ 2),(- (z * F))) is Element of the carrier of p
((z |^ 2) - (z * F)) + (F * (z - F)) is Element of the carrier of p
the addF of p . (((z |^ 2) - (z * F)),(F * (z - F))) is Element of the carrier of p
F * z is Element of the carrier of p
the multF of p . (F,z) is Element of the carrier of p
F * F is Element of the carrier of p
the multF of p . (F,F) is Element of the carrier of p
(F * z) - (F * F) is Element of the carrier of p
- (F * F) is Element of the carrier of p
(F * z) + (- (F * F)) is Element of the carrier of p
the addF of p . ((F * z),(- (F * F))) is Element of the carrier of p
((z |^ 2) - (z * F)) + ((F * z) - (F * F)) is Element of the carrier of p
the addF of p . (((z |^ 2) - (z * F)),((F * z) - (F * F))) is Element of the carrier of p
(z * F) - (F |^ 2) is Element of the carrier of p
(z * F) + (- (F |^ 2)) is Element of the carrier of p
the addF of p . ((z * F),(- (F |^ 2))) is Element of the carrier of p
((z |^ 2) - (z * F)) + ((z * F) - (F |^ 2)) is Element of the carrier of p
the addF of p . (((z |^ 2) - (z * F)),((z * F) - (F |^ 2))) is Element of the carrier of p
(- (z * F)) + ((z * F) - (F |^ 2)) is Element of the carrier of p
the addF of p . ((- (z * F)),((z * F) - (F |^ 2))) is Element of the carrier of p
(z |^ 2) + ((- (z * F)) + ((z * F) - (F |^ 2))) is Element of the carrier of p
the addF of p . ((z |^ 2),((- (z * F)) + ((z * F) - (F |^ 2)))) is Element of the carrier of p
(- (z * F)) + (z * F) is Element of the carrier of p
the addF of p . ((- (z * F)),(z * F)) is Element of the carrier of p
((- (z * F)) + (z * F)) - (F |^ 2) is Element of the carrier of p
((- (z * F)) + (z * F)) + (- (F |^ 2)) is Element of the carrier of p
the addF of p . (((- (z * F)) + (z * F)),(- (F |^ 2))) is Element of the carrier of p
(z |^ 2) + (((- (z * F)) + (z * F)) - (F |^ 2)) is Element of the carrier of p
the addF of p . ((z |^ 2),(((- (z * F)) + (z * F)) - (F |^ 2))) is Element of the carrier of p
0. p is V55(p) Element of the carrier of p
(0. p) - (F |^ 2) is Element of the carrier of p
(0. p) + (- (F |^ 2)) is Element of the carrier of p
the addF of p . ((0. p),(- (F |^ 2))) is Element of the carrier of p
(z |^ 2) + ((0. p) - (F |^ 2)) is Element of the carrier of p
the addF of p . ((z |^ 2),((0. p) - (F |^ 2))) is Element of the carrier of p
p is non empty non degenerated non trivial right_complementable almost_left_invertible V147() V148() V149() unital V166() V168() V170() right-distributive left-distributive right_unital well-unital V183() left_unital doubleLoopStr
the carrier of p is non empty non trivial set
z is Element of the carrier of p
z |^ 2 is Element of the carrier of p
power p is V18() Function-like V32([: the carrier of p,NAT:], the carrier of p) Element of bool [:[: the carrier of p,NAT:], the carrier of p:]
[: the carrier of p,NAT:] is non empty V18() set
[:[: the carrier of p,NAT:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p,NAT:], the carrier of p:] is non empty set
(power p) . (z,2) is set
z |^ 3 is Element of the carrier of p
(power p) . (z,3) is set
F is Element of the carrier of p
z + F is Element of the carrier of p
the addF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty V18() set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty V18() set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the addF of p . (z,F) is Element of the carrier of p
z * F is Element of the carrier of p
the multF of p is V18() Function-like V32([: the carrier of p, the carrier of p:], the carrier of p) Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
the multF of p . (z,F) is Element of the carrier of p
(z |^ 2) - (z * F) is Element of the carrier of p
- (z * F) is Element of the carrier of p
(z |^ 2) + (- (z * F)) is Element of the carrier of p
the addF of p . ((z |^ 2),(- (z * F))) is Element of the carrier of p
F |^ 2 is Element of the carrier of p
(power p) . (F,2) is set
((z |^ 2) - (z * F)) + (F |^ 2) is Element of the carrier of p
the addF of p . (((z |^ 2) - (z * F)),(F |^ 2)) is Element of the carrier of p
(z + F) * (((z |^ 2) - (z * F)) + (F |^ 2)) is Element of the carrier of p
the multF of p . ((z + F),(((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
F |^ 3 is Element of the carrier of p
(power p) . (F,3) is set
(z |^ 3) + (F |^ 3) is Element of the carrier of p
the addF of p . ((z |^ 3),(F |^ 3)) is Element of the carrier of p
z * (((z |^ 2) - (z * F)) + (F |^ 2)) is Element of the carrier of p
the multF of p . (z,(((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
F * (((z |^ 2) - (z * F)) + (F |^ 2)) is Element of the carrier of p
the multF of p . (F,(((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
(z * (((z |^ 2) - (z * F)) + (F |^ 2))) + (F * (((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
the addF of p . ((z * (((z |^ 2) - (z * F)) + (F |^ 2))),(F * (((z |^ 2) - (z * F)) + (F |^ 2)))) is Element of the carrier of p
z * ((z |^ 2) - (z * F)) is Element of the carrier of p
the multF of p . (z,((z |^ 2) - (z * F))) is Element of the carrier of p
z * (F |^ 2) is Element of the carrier of p
the multF of p . (z,(F |^ 2)) is Element of the carrier of p
(z * ((z |^ 2) - (z * F))) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . ((z * ((z |^ 2) - (z * F))),(z * (F |^ 2))) is Element of the carrier of p
((z * ((z |^ 2) - (z * F))) + (z * (F |^ 2))) + (F * (((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
the addF of p . (((z * ((z |^ 2) - (z * F))) + (z * (F |^ 2))),(F * (((z |^ 2) - (z * F)) + (F |^ 2)))) is Element of the carrier of p
z * (z |^ 2) is Element of the carrier of p
the multF of p . (z,(z |^ 2)) is Element of the carrier of p
z * (z * F) is Element of the carrier of p
the multF of p . (z,(z * F)) is Element of the carrier of p
(z * (z |^ 2)) - (z * (z * F)) is Element of the carrier of p
- (z * (z * F)) is Element of the carrier of p
(z * (z |^ 2)) + (- (z * (z * F))) is Element of the carrier of p
the addF of p . ((z * (z |^ 2)),(- (z * (z * F)))) is Element of the carrier of p
((z * (z |^ 2)) - (z * (z * F))) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . (((z * (z |^ 2)) - (z * (z * F))),(z * (F |^ 2))) is Element of the carrier of p
(((z * (z |^ 2)) - (z * (z * F))) + (z * (F |^ 2))) + (F * (((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
the addF of p . ((((z * (z |^ 2)) - (z * (z * F))) + (z * (F |^ 2))),(F * (((z |^ 2) - (z * F)) + (F |^ 2)))) is Element of the carrier of p
(z |^ 2) * z is Element of the carrier of p
the multF of p . ((z |^ 2),z) is Element of the carrier of p
z * z is Element of the carrier of p
the multF of p . (z,z) is Element of the carrier of p
(z * z) * F is Element of the carrier of p
the multF of p . ((z * z),F) is Element of the carrier of p
((z |^ 2) * z) - ((z * z) * F) is Element of the carrier of p
- ((z * z) * F) is Element of the carrier of p
((z |^ 2) * z) + (- ((z * z) * F)) is Element of the carrier of p
the addF of p . (((z |^ 2) * z),(- ((z * z) * F))) is Element of the carrier of p
(((z |^ 2) * z) - ((z * z) * F)) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . ((((z |^ 2) * z) - ((z * z) * F)),(z * (F |^ 2))) is Element of the carrier of p
((((z |^ 2) * z) - ((z * z) * F)) + (z * (F |^ 2))) + (F * (((z |^ 2) - (z * F)) + (F |^ 2))) is Element of the carrier of p
the addF of p . (((((z |^ 2) * z) - ((z * z) * F)) + (z * (F |^ 2))),(F * (((z |^ 2) - (z * F)) + (F |^ 2)))) is Element of the carrier of p
F * ((z |^ 2) - (z * F)) is Element of the carrier of p
the multF of p . (F,((z |^ 2) - (z * F))) is Element of the carrier of p
F * (F |^ 2) is Element of the carrier of p
the multF of p . (F,(F |^ 2)) is Element of the carrier of p
(F * ((z |^ 2) - (z * F))) + (F * (F |^ 2)) is Element of the carrier of p
the addF of p . ((F * ((z |^ 2) - (z * F))),(F * (F |^ 2))) is Element of the carrier of p
((((z |^ 2) * z) - ((z * z) * F)) + (z * (F |^ 2))) + ((F * ((z |^ 2) - (z * F))) + (F * (F |^ 2))) is Element of the carrier of p
the addF of p . (((((z |^ 2) * z) - ((z * z) * F)) + (z * (F |^ 2))),((F * ((z |^ 2) - (z * F))) + (F * (F |^ 2)))) is Element of the carrier of p
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real Element of NAT
z |^ (2 + 1) is Element of the carrier of p
(power p) . (z,(2 + 1)) is set
(z |^ (2 + 1)) - ((z * z) * F) is Element of the carrier of p
(z |^ (2 + 1)) + (- ((z * z) * F)) is Element of the carrier of p
the addF of p . ((z |^ (2 + 1)),(- ((z * z) * F))) is Element of the carrier of p
((z |^ (2 + 1)) - ((z * z) * F)) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . (((z |^ (2 + 1)) - ((z * z) * F)),(z * (F |^ 2))) is Element of the carrier of p
(F |^ 2) * F is Element of the carrier of p
the multF of p . ((F |^ 2),F) is Element of the carrier of p
(F * ((z |^ 2) - (z * F))) + ((F |^ 2) * F) is Element of the carrier of p
the addF of p . ((F * ((z |^ 2) - (z * F))),((F |^ 2) * F)) is Element of the carrier of p
(((z |^ (2 + 1)) - ((z * z) * F)) + (z * (F |^ 2))) + ((F * ((z |^ 2) - (z * F))) + ((F |^ 2) * F)) is Element of the carrier of p
the addF of p . ((((z |^ (2 + 1)) - ((z * z) * F)) + (z * (F |^ 2))),((F * ((z |^ 2) - (z * F))) + ((F |^ 2) * F))) is Element of the carrier of p
(z |^ 3) - ((z * z) * F) is Element of the carrier of p
(z |^ 3) + (- ((z * z) * F)) is Element of the carrier of p
the addF of p . ((z |^ 3),(- ((z * z) * F))) is Element of the carrier of p
((z |^ 3) - ((z * z) * F)) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . (((z |^ 3) - ((z * z) * F)),(z * (F |^ 2))) is Element of the carrier of p
F * (z |^ 2) is Element of the carrier of p
the multF of p . (F,(z |^ 2)) is Element of the carrier of p
F * (z * F) is Element of the carrier of p
the multF of p . (F,(z * F)) is Element of the carrier of p
(F * (z |^ 2)) - (F * (z * F)) is Element of the carrier of p
- (F * (z * F)) is Element of the carrier of p
(F * (z |^ 2)) + (- (F * (z * F))) is Element of the carrier of p
the addF of p . ((F * (z |^ 2)),(- (F * (z * F)))) is Element of the carrier of p
((F * (z |^ 2)) - (F * (z * F))) + ((F |^ 2) * F) is Element of the carrier of p
the addF of p . (((F * (z |^ 2)) - (F * (z * F))),((F |^ 2) * F)) is Element of the carrier of p
(((z |^ 3) - ((z * z) * F)) + (z * (F |^ 2))) + (((F * (z |^ 2)) - (F * (z * F))) + ((F |^ 2) * F)) is Element of the carrier of p
the addF of p . ((((z |^ 3) - ((z * z) * F)) + (z * (F |^ 2))),(((F * (z |^ 2)) - (F * (z * F))) + ((F |^ 2) * F))) is Element of the carrier of p
(z |^ 2) * F is Element of the carrier of p
the multF of p . ((z |^ 2),F) is Element of the carrier of p
(z |^ 3) - ((z |^ 2) * F) is Element of the carrier of p
- ((z |^ 2) * F) is Element of the carrier of p
(z |^ 3) + (- ((z |^ 2) * F)) is Element of the carrier of p
the addF of p . ((z |^ 3),(- ((z |^ 2) * F))) is Element of the carrier of p
((z |^ 3) - ((z |^ 2) * F)) + (z * (F |^ 2)) is Element of the carrier of p
the addF of p . (((z |^ 3) - ((z |^ 2) * F)),(z * (F |^ 2))) is Element of the carrier of p
(((z |^ 3) - ((z |^ 2) * F)) + (z * (F |^ 2))) + (((F * (z |^ 2)) - (F * (z * F))) + ((F |^ 2) * F)) is Element of the carrier of p
the addF of p . ((((z |^ 3) - ((z |^ 2) * F)) + (z * (F |^ 2))),(((F * (z |^ 2)) - (F * (z * F))) + ((F |^ 2) * F))) is Element of the carrier of p
(z * F) * F is Element of the carrier of p
the multF of p . ((z * F),F) is Element of the carrier of p
((z |^ 2) * F) - ((z * F) * F) is Element of the carrier of p
- ((z * F) * F) is Element of the carrier of p
((z |^ 2) * F) + (- ((z * F) * F)) is Element of the carrier of p
the addF of p . (((z |^ 2) * F),(- ((z * F) * F))) is Element of the carrier of p
F |^ (2 + 1) is Element of the carrier of p
(power p) . (F,(2 + 1)) is set
(((z |^ 2) * F) - ((z * F) * F)) + (F |^ (2 + 1)) is Element of the carrier of p
the addF of p . ((((z |^ 2) * F) - ((z * F) * F)),(F |^ (2 + 1))) is Element of the carrier of p
(((z |^ 3) - ((z |^ 2) * F)) + (z * (F |^ 2))) + ((((z |^ 2) * F) - ((z * F) * F)) + (F |^ (2 + 1))) is Element of the carrier of p
the addF of p . ((((z |^ 3) - ((z |^ 2) * F))