:: POLYALG1 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of bool REAL
bool REAL is non empty set
K425() is strict V192() doubleLoopStr
the carrier of K425() is set
NAT is non empty V24() V25() V26() set
bool NAT is non empty set
bool NAT is non empty set
COMPLEX is set
RAT is set
INT is set
2 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative Element of NAT
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative Element of NAT
K285(1,NAT) is M15( NAT )
{} is Relation-like non-empty empty-yielding functional empty V24() V25() V26() V28() V29() V30() FinSequence-like FinSequence-membered V42() V43() ext-real non negative set
3 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding functional empty V24() V25() V26() V28() V29() V30() FinSequence-like FinSequence-membered V42() V43() ext-real non negative Element of NAT
len {} is V36() set
L is non empty doubleLoopStr
{0} is non empty set
the carrier of L is non empty set
[: the carrier of L,{0}:] is Relation-like non empty set
[:[: the carrier of L,{0}:],{0}:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],{0}:] is non empty set
[: the carrier of L,{0}:] --> 0 is Relation-like [: the carrier of L,{0}:] -defined NAT -valued Function-like non empty total V18([: the carrier of L,{0}:], NAT ) Element of bool [:[: the carrier of L,{0}:],NAT:]
[:[: the carrier of L,{0}:],NAT:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],NAT:] is non empty set
[:{0},{0}:] is Relation-like non empty set
[:[:{0},{0}:],{0}:] is Relation-like non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]
y is Element of {0}
x is Relation-like [: the carrier of L,{0}:] -defined {0} -valued Function-like non empty total V18([: the carrier of L,{0}:],{0}) Element of bool [:[: the carrier of L,{0}:],{0}:]
(L,{0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:], the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:],y,y,x) is (L) (L)
L is non empty doubleLoopStr
L is non empty doubleLoopStr
{0} is non empty set
the carrier of L is non empty set
[: the carrier of L,{0}:] is Relation-like non empty set
[:[: the carrier of L,{0}:],{0}:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],{0}:] is non empty set
[: the carrier of L,{0}:] --> 0 is Relation-like [: the carrier of L,{0}:] -defined NAT -valued Function-like non empty total V18([: the carrier of L,{0}:], NAT ) Element of bool [:[: the carrier of L,{0}:],NAT:]
[:[: the carrier of L,{0}:],NAT:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],NAT:] is non empty set
[:{0},{0}:] is Relation-like non empty set
[:[:{0},{0}:],{0}:] is Relation-like non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]
y is Element of {0}
x is Relation-like [: the carrier of L,{0}:] -defined {0} -valued Function-like non empty total V18([: the carrier of L,{0}:],{0}) Element of bool [:[: the carrier of L,{0}:],{0}:]
(L,{0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:], the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:],y,y,x) is (L) (L)
y9 is non empty (L)
the carrier of y9 is non empty set
x9 is Element of the carrier of y9
p is Element of the carrier of y9
1. y9 is Element of the carrier of y9
the OneF of y9 is Element of the carrier of y9
x9 is Element of the carrier of y9
x9 * (1. y9) is Element of the carrier of y9
the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the multF of y9 . (x9,(1. y9)) is Element of the carrier of y9
[x9,(1. y9)] is set
{x9,(1. y9)} is non empty set
{x9} is non empty set
{{x9,(1. y9)},{x9}} is non empty set
the multF of y9 . [x9,(1. y9)] is set
p is Element of the carrier of y9
(1. y9) * p is Element of the carrier of y9
the multF of y9 . ((1. y9),p) is Element of the carrier of y9
[(1. y9),p] is set
{(1. y9),p} is non empty set
{(1. y9)} is non empty set
{{(1. y9),p},{(1. y9)}} is non empty set
the multF of y9 . [(1. y9),p] is set
x9 is Element of the carrier of y9
p is Element of the carrier of y9
x1 is Element of the carrier of y9
p + x1 is Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the addF of y9 . (p,x1) is Element of the carrier of y9
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the addF of y9 . [p,x1] is set
x9 * (p + x1) is Element of the carrier of y9
the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
the multF of y9 . (x9,(p + x1)) is Element of the carrier of y9
[x9,(p + x1)] is set
{x9,(p + x1)} is non empty set
{x9} is non empty set
{{x9,(p + x1)},{x9}} is non empty set
the multF of y9 . [x9,(p + x1)] is set
x9 * p is Element of the carrier of y9
the multF of y9 . (x9,p) is Element of the carrier of y9
[x9,p] is set
{x9,p} is non empty set
{{x9,p},{x9}} is non empty set
the multF of y9 . [x9,p] is set
x9 * x1 is Element of the carrier of y9
the multF of y9 . (x9,x1) is Element of the carrier of y9
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the multF of y9 . [x9,x1] is set
(x9 * p) + (x9 * x1) is Element of the carrier of y9
the addF of y9 . ((x9 * p),(x9 * x1)) is Element of the carrier of y9
[(x9 * p),(x9 * x1)] is set
{(x9 * p),(x9 * x1)} is non empty set
{(x9 * p)} is non empty set
{{(x9 * p),(x9 * x1)},{(x9 * p)}} is non empty set
the addF of y9 . [(x9 * p),(x9 * x1)] is set
(p + x1) * x9 is Element of the carrier of y9
the multF of y9 . ((p + x1),x9) is Element of the carrier of y9
[(p + x1),x9] is set
{(p + x1),x9} is non empty set
{(p + x1)} is non empty set
{{(p + x1),x9},{(p + x1)}} is non empty set
the multF of y9 . [(p + x1),x9] is set
p * x9 is Element of the carrier of y9
the multF of y9 . (p,x9) is Element of the carrier of y9
[p,x9] is set
{p,x9} is non empty set
{{p,x9},{p}} is non empty set
the multF of y9 . [p,x9] is set
x1 * x9 is Element of the carrier of y9
the multF of y9 . (x1,x9) is Element of the carrier of y9
[x1,x9] is set
{x1,x9} is non empty set
{x1} is non empty set
{{x1,x9},{x1}} is non empty set
the multF of y9 . [x1,x9] is set
(p * x9) + (x1 * x9) is Element of the carrier of y9
the addF of y9 . ((p * x9),(x1 * x9)) is Element of the carrier of y9
[(p * x9),(x1 * x9)] is set
{(p * x9),(x1 * x9)} is non empty set
{(p * x9)} is non empty set
{{(p * x9),(x1 * x9)},{(p * x9)}} is non empty set
the addF of y9 . [(p * x9),(x1 * x9)] is set
x9 is Element of the carrier of L
p is Element of the carrier of y9
x1 is Element of the carrier of y9
p + x1 is Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the addF of y9 . (p,x1) is Element of the carrier of y9
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the addF of y9 . [p,x1] is set
x9 * (p + x1) is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . (x9,(p + x1)) is Element of the carrier of y9
[x9,(p + x1)] is set
{x9,(p + x1)} is non empty set
{x9} is non empty set
{{x9,(p + x1)},{x9}} is non empty set
the lmult of y9 . [x9,(p + x1)] is set
x9 * p is Element of the carrier of y9
the lmult of y9 . (x9,p) is Element of the carrier of y9
[x9,p] is set
{x9,p} is non empty set
{{x9,p},{x9}} is non empty set
the lmult of y9 . [x9,p] is set
x9 * x1 is Element of the carrier of y9
the lmult of y9 . (x9,x1) is Element of the carrier of y9
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the lmult of y9 . [x9,x1] is set
(x9 * p) + (x9 * x1) is Element of the carrier of y9
the addF of y9 . ((x9 * p),(x9 * x1)) is Element of the carrier of y9
[(x9 * p),(x9 * x1)] is set
{(x9 * p),(x9 * x1)} is non empty set
{(x9 * p)} is non empty set
{{(x9 * p),(x9 * x1)},{(x9 * p)}} is non empty set
the addF of y9 . [(x9 * p),(x9 * x1)] is set
x9 is Element of the carrier of L
p is Element of the carrier of L
x9 + p is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x9,p) is Element of the carrier of L
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the addF of L . [x9,p] is set
x1 is Element of the carrier of y9
(x9 + p) * x1 is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . ((x9 + p),x1) is Element of the carrier of y9
[(x9 + p),x1] is set
{(x9 + p),x1} is non empty set
{(x9 + p)} is non empty set
{{(x9 + p),x1},{(x9 + p)}} is non empty set
the lmult of y9 . [(x9 + p),x1] is set
x9 * x1 is Element of the carrier of y9
the lmult of y9 . (x9,x1) is Element of the carrier of y9
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the lmult of y9 . [x9,x1] is set
p * x1 is Element of the carrier of y9
the lmult of y9 . (p,x1) is Element of the carrier of y9
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the lmult of y9 . [p,x1] is set
(x9 * x1) + (p * x1) is Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the addF of y9 . ((x9 * x1),(p * x1)) is Element of the carrier of y9
[(x9 * x1),(p * x1)] is set
{(x9 * x1),(p * x1)} is non empty set
{(x9 * x1)} is non empty set
{{(x9 * x1),(p * x1)},{(x9 * x1)}} is non empty set
the addF of y9 . [(x9 * x1),(p * x1)] is set
x9 is Element of the carrier of L
p is Element of the carrier of L
x9 * p is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x9,p) is Element of the carrier of L
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the multF of L . [x9,p] is set
x1 is Element of the carrier of y9
(x9 * p) * x1 is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . ((x9 * p),x1) is Element of the carrier of y9
[(x9 * p),x1] is set
{(x9 * p),x1} is non empty set
{(x9 * p)} is non empty set
{{(x9 * p),x1},{(x9 * p)}} is non empty set
the lmult of y9 . [(x9 * p),x1] is set
p * x1 is Element of the carrier of y9
the lmult of y9 . (p,x1) is Element of the carrier of y9
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the lmult of y9 . [p,x1] is set
x9 * (p * x1) is Element of the carrier of y9
the lmult of y9 . (x9,(p * x1)) is Element of the carrier of y9
[x9,(p * x1)] is set
{x9,(p * x1)} is non empty set
{{x9,(p * x1)},{x9}} is non empty set
the lmult of y9 . [x9,(p * x1)] is set
1. L is Element of the carrier of L
the OneF of L is Element of the carrier of L
x9 is Element of the carrier of y9
(1. L) * x9 is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . ((1. L),x9) is Element of the carrier of y9
[(1. L),x9] is set
{(1. L),x9} is non empty set
{(1. L)} is non empty set
{{(1. L),x9},{(1. L)}} is non empty set
the lmult of y9 . [(1. L),x9] is set
x9 is Element of the carrier of L
p is Element of the carrier of y9
x1 is Element of the carrier of y9
p * x1 is Element of the carrier of y9
the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the multF of y9 . (p,x1) is Element of the carrier of y9
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the multF of y9 . [p,x1] is set
x9 * (p * x1) is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . (x9,(p * x1)) is Element of the carrier of y9
[x9,(p * x1)] is set
{x9,(p * x1)} is non empty set
{x9} is non empty set
{{x9,(p * x1)},{x9}} is non empty set
the lmult of y9 . [x9,(p * x1)] is set
x9 * p is Element of the carrier of y9
the lmult of y9 . (x9,p) is Element of the carrier of y9
[x9,p] is set
{x9,p} is non empty set
{{x9,p},{x9}} is non empty set
the lmult of y9 . [x9,p] is set
(x9 * p) * x1 is Element of the carrier of y9
the multF of y9 . ((x9 * p),x1) is Element of the carrier of y9
[(x9 * p),x1] is set
{(x9 * p),x1} is non empty set
{(x9 * p)} is non empty set
{{(x9 * p),x1},{(x9 * p)}} is non empty set
the multF of y9 . [(x9 * p),x1] is set
L is set
x is set
[:L,x:] is Relation-like set
[:[:L,x:],L:] is Relation-like set
bool [:[:L,x:],L:] is non empty set
y is Relation-like [:L,x:] -defined L -valued Function-like V18([:L,x:],L) Element of bool [:[:L,x:],L:]
dom y is Relation-like set
L is set
x is set
[:L,x:] is Relation-like set
[:[:L,x:],x:] is Relation-like set
bool [:[:L,x:],x:] is non empty set
y is Relation-like [:L,x:] -defined x -valued Function-like V18([:L,x:],x) Element of bool [:[:L,x:],x:]
dom y is Relation-like set
L is non empty doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
{ b₁ where b₁ is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:] : verum } is set
x is non empty set
y1 is Element of x
y9 is Element of x
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Element of x
[:x,x:] is Relation-like non empty set
[:[:x,x:],x:] is Relation-like non empty set
bool [:[:x,x:],x:] is non empty set
y1 is Relation-like [:x,x:] -defined x -valued Function-like non empty total V18([:x,x:],x) Element of bool [:[:x,x:],x:]
x9 is Element of x
p is Element of x
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 *' q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 is Element of x
x9 is Relation-like [:x,x:] -defined x -valued Function-like non empty total V18([:x,x:],x) Element of bool [:[:x,x:],x:]
p is Element of the carrier of L
x1 is Element of x
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p * q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 is Element of x
[: the carrier of L,x:] is Relation-like non empty set
[:[: the carrier of L,x:],x:] is Relation-like non empty set
bool [:[: the carrier of L,x:],x:] is non empty set
p is Relation-like [: the carrier of L,x:] -defined x -valued Function-like non empty total V18([: the carrier of L,x:],x) Element of bool [:[: the carrier of L,x:],x:]
y is Element of x
y9 is Element of x
(L,x,y1,x9,y,y9,p) is (L) (L)
x1 is non empty (L) (L)
the carrier of x1 is non empty set
0. x1 is V54(x1) Element of the carrier of x1
the ZeroF of x1 is Element of the carrier of x1
1. x1 is Element of the carrier of x1
the OneF of x1 is Element of the carrier of x1
q is set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Element of the carrier of x1
x9 is Element of the carrier of x1
q + x9 is Element of the carrier of x1
the addF of x1 is Relation-like [: the carrier of x1, the carrier of x1:] -defined the carrier of x1 -valued Function-like non empty total V18([: the carrier of x1, the carrier of x1:], the carrier of x1) Element of bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:]
[: the carrier of x1, the carrier of x1:] is Relation-like non empty set
[:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is Relation-like non empty set
bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is non empty set
the addF of x1 . (q,x9) is Element of the carrier of x1
[q,x9] is set
{q,x9} is non empty set
{q} is non empty set
{{q,x9},{q}} is non empty set
the addF of x1 . [q,x9] is set
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 + x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 . (q,x9) is set
y1 . [q,x9] is set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
c₁₄ is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 + c₁₄ is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Element of the carrier of x1
x9 is Element of the carrier of x1
q * x9 is Element of the carrier of x1
the multF of x1 is Relation-like [: the carrier of x1, the carrier of x1:] -defined the carrier of x1 -valued Function-like non empty total V18([: the carrier of x1, the carrier of x1:], the carrier of x1) Element of bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:]
[: the carrier of x1, the carrier of x1:] is Relation-like non empty set
[:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is Relation-like non empty set
bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is non empty set
the multF of x1 . (q,x9) is Element of the carrier of x1
[q,x9] is set
{q,x9} is non empty set
{q} is non empty set
{{q,x9},{q}} is non empty set
the multF of x1 . [q,x9] is set
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 . (q,x9) is set
x9 . [q,x9] is set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
c₁₄ is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 *' c₁₄ is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Element of the carrier of L
x9 is Element of the carrier of x1
q * x9 is Element of the carrier of x1
the lmult of x1 is Relation-like [: the carrier of L, the carrier of x1:] -defined the carrier of x1 -valued Function-like non empty total V18([: the carrier of L, the carrier of x1:], the carrier of x1) Element of bool [:[: the carrier of L, the carrier of x1:], the carrier of x1:]
[: the carrier of L, the carrier of x1:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x1:], the carrier of x1:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x1:], the carrier of x1:] is non empty set
the lmult of x1 . (q,x9) is Element of the carrier of x1
[q,x9] is set
{q,x9} is non empty set
{q} is non empty set
{{q,x9},{q}} is non empty set
the lmult of x1 . [q,x9] is set
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q * y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p . (q,x9) is set
p . [q,x9] is set
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q * x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x is non empty (L) (L)
the carrier of x is non empty set
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
y is non empty (L) (L)
the carrier of y is non empty set
0. y is V54(y) Element of the carrier of y
the ZeroF of y is Element of the carrier of y
1. y is Element of the carrier of y
the OneF of y is Element of the carrier of y
y1 is set
y9 is Element of the carrier of x
y1 is Element of the carrier of L
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x . (y1,y9) is Element of the carrier of x
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the lmult of x . [y1,y9] is set
y1 * y9 is Element of the carrier of x
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Element of the carrier of L
x1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Element of the carrier of y
x1 * p is Element of the carrier of y
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[: the carrier of L, the carrier of y:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
the lmult of y . (x1,p) is Element of the carrier of y
[x1,p] is set
{x1,p} is non empty set
{x1} is non empty set
{{x1,p},{x1}} is non empty set
the lmult of y . [x1,p] is set
the lmult of y . (y1,y9) is set
the lmult of y . [y1,y9] is set
y9 is Element of the carrier of y
y1 is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (y1,y9) is set
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the multF of x . [y1,y9] is set
x9 is Element of the carrier of x
y1 * x9 is Element of the carrier of x
the multF of x . (y1,x9) is Element of the carrier of x
[y1,x9] is set
{y1,x9} is non empty set
{{y1,x9},{y1}} is non empty set
the multF of x . [y1,x9] is set
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 *' q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Element of the carrier of y
p * y9 is Element of the carrier of y
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the multF of y . (p,y9) is Element of the carrier of y
[p,y9] is set
{p,y9} is non empty set
{p} is non empty set
{{p,y9},{p}} is non empty set
the multF of y . [p,y9] is set
the multF of y . (y1,y9) is set
the multF of y . [y1,y9] is set
y9 is Element of the carrier of y
y1 is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . (y1,y9) is set
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the addF of x . [y1,y9] is set
x9 is Element of the carrier of x
y1 + x9 is Element of the carrier of x
the addF of x . (y1,x9) is Element of the carrier of x
[y1,x9] is set
{y1,x9} is non empty set
{{y1,x9},{y1}} is non empty set
the addF of x . [y1,x9] is set
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 + q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Element of the carrier of y
p + y9 is Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
the addF of y . (p,y9) is Element of the carrier of y
[p,y9] is set
{p,y9} is non empty set
{p} is non empty set
{{p,y9},{p}} is non empty set
the addF of y . [p,y9] is set
the addF of y . (y1,y9) is set
the addF of y . [y1,y9] is set
L is non empty Abelian doubleLoopStr
(L) is non empty (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (L)
x + y is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of (L) . [x,y] is set
y + x is Element of the carrier of (L)
the addF of (L) . (y,x) is Element of the carrier of (L)
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the addF of (L) . [y,x] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 + y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty add-associative doubleLoopStr
(L) is non empty (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (L)
x + y is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of (L) . [x,y] is set
y1 is Element of the carrier of (L)
(x + y) + y1 is Element of the carrier of (L)
the addF of (L) . ((x + y),y1) is Element of the carrier of (L)
[(x + y),y1] is set
{(x + y),y1} is non empty set
{(x + y)} is non empty set
{{(x + y),y1},{(x + y)}} is non empty set
the addF of (L) . [(x + y),y1] is set
y + y1 is Element of the carrier of (L)
the addF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the addF of (L) . [y,y1] is set
x + (y + y1) is Element of the carrier of (L)
the addF of (L) . (x,(y + y1)) is Element of the carrier of (L)
[x,(y + y1)] is set
{x,(y + y1)} is non empty set
{{x,(y + y1)},{x}} is non empty set
the addF of (L) . [x,(y + y1)] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 + x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y9 + x9) + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 + (x9 + p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty right_zeroed doubleLoopStr
(L) is non empty (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
0. (L) is V54((L)) Element of the carrier of (L)
the ZeroF of (L) is Element of the carrier of (L)
x + (0. (L)) is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (x,(0. (L))) is Element of the carrier of (L)
[x,(0. (L))] is set
{x,(0. (L))} is non empty set
{x} is non empty set
{{x,(0. (L))},{x}} is non empty set
the addF of (L) . [x,(0. (L))] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y + (0_. L) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty right_add-cancelable right_complementable add-associative right_zeroed doubleLoopStr
(L) is non empty add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
- y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 is Element of the carrier of (L)
x + y1 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (x,y1) is Element of the carrier of (L)
[x,y1] is set
{x,y1} is non empty set
{x} is non empty set
{{x,y1},{x}} is non empty set
the addF of (L) . [x,y1] is set
0. (L) is V54((L)) Element of the carrier of (L)
the ZeroF of (L) is Element of the carrier of (L)
y + (- y) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y - y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
L is non empty left_zeroed commutative Abelian add-associative right_zeroed doubleLoopStr
(L) is non empty left_zeroed Abelian add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (L)
x * y is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of (L) . [x,y] is set
y * x is Element of the carrier of (L)
the multF of (L) . (y,x) is Element of the carrier of (L)
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the multF of (L) . [y,x] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 *' y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(L) is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed Abelian add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (L)
x * y is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of (L) . [x,y] is set
y1 is Element of the carrier of (L)
(x * y) * y1 is Element of the carrier of (L)
the multF of (L) . ((x * y),y1) is Element of the carrier of (L)
[(x * y),y1] is set
{(x * y),y1} is non empty set
{(x * y)} is non empty set
{{(x * y),y1},{(x * y)}} is non empty set
the multF of (L) . [(x * y),y1] is set
y * y1 is Element of the carrier of (L)
the multF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the multF of (L) . [y,y1] is set
x * (y * y1) is Element of the carrier of (L)
the multF of (L) . (x,(y * y1)) is Element of the carrier of (L)
[x,(y * y1)] is set
{x,(y * y1)} is non empty set
{{x,(y * y1)},{x}} is non empty set
the multF of (L) . [x,(y * y1)] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 *' p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y9 *' x9) *' p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' (x9 *' p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
F_Real is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict left_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
L is non empty set
x is Relation-like NAT -defined L -valued Function-like non empty V31() FinSequence-like FinSubsequence-like FinSequence of L
x /^ 1 is Relation-like NAT -defined L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of L
Del (x,1) is Relation-like NAT -defined L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of L
len x is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y is V24() V25() V26() V30() V42() V43() ext-real non negative set
y + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
len (x /^ 1) is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
len (Del (x,1)) is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y1 + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
(y1 + 1) - 1 is V42() V43() ext-real set
dom x is non empty Element of bool NAT
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative set
(x /^ 1) . y9 is set
(Del (x,1)) . y9 is set
dom (x /^ 1) is Element of bool NAT
y9 + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
x . (y9 + 1) is set
L is non empty set
x is Relation-like NAT -defined L -valued Function-like non empty V31() FinSequence-like FinSubsequence-like FinSequence of L
x . 1 is set
<*(x . 1)*> is Relation-like NAT -defined Function-like non empty V31() V38(1) FinSequence-like FinSubsequence-like set
Del (x,1) is Relation-like NAT -defined L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of L
<*(x . 1)*> ^ (Del (x,1)) is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set
dom x is non empty Element of bool NAT
x /. 1 is Element of L
<*(x /. 1)*> is Relation-like NAT -defined L -valued Function-like non empty V31() V38(1) FinSequence-like FinSubsequence-like FinSequence of L
x /^ 1 is Relation-like NAT -defined L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of L
<*(x /. 1)*> ^ (x /^ 1) is Relation-like NAT -defined L -valued Function-like non empty V31() FinSequence-like FinSubsequence-like FinSequence of L
<*(x . 1)*> ^ (x /^ 1) is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set
L is non empty right_add-cancelable right_complementable unital left-distributive right_unital well-unital left_unital add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(1_. L) *' x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
((1_. L) *' x) . y is Element of the carrier of L
y1 is Relation-like NAT -defined the carrier of L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len y1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
Sum y1 is Element of the carrier of L
dom y1 is Element of bool NAT
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y9 + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
Del (y1,1) is Relation-like NAT -defined the carrier of L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
dom (Del (y1,1)) is Element of bool NAT
len (Del (y1,1)) is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
(Del (y1,1)) . y9 is set
y1 . (y9 + 1) is set
(y9 + 1) -' 1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
(1_. L) . ((y9 + 1) -' 1) is Element of the carrier of L
(y + 1) -' (y9 + 1) is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
x . ((y + 1) -' (y9 + 1)) is Element of the carrier of L
((1_. L) . ((y9 + 1) -' 1)) * (x . ((y + 1) -' (y9 + 1))) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (((1_. L) . ((y9 + 1) -' 1)),(x . ((y + 1) -' (y9 + 1)))) is Element of the carrier of L
[((1_. L) . ((y9 + 1) -' 1)),(x . ((y + 1) -' (y9 + 1)))] is set
{((1_. L) . ((y9 + 1) -' 1)),(x . ((y + 1) -' (y9 + 1)))} is non empty set
{((1_. L) . ((y9 + 1) -' 1))} is non empty set
{{((1_. L) . ((y9 + 1) -' 1)),(x . ((y + 1) -' (y9 + 1)))},{((1_. L) . ((y9 + 1) -' 1))}} is non empty set
the multF of L . [((1_. L) . ((y9 + 1) -' 1)),(x . ((y + 1) -' (y9 + 1)))] is set
(1_. L) . y9 is Element of the carrier of L
((1_. L) . y9) * (x . ((y + 1) -' (y9 + 1))) is Element of the carrier of L
the multF of L . (((1_. L) . y9),(x . ((y + 1) -' (y9 + 1)))) is Element of the carrier of L
[((1_. L) . y9),(x . ((y + 1) -' (y9 + 1)))] is set
{((1_. L) . y9),(x . ((y + 1) -' (y9 + 1)))} is non empty set
{((1_. L) . y9)} is non empty set
{{((1_. L) . y9),(x . ((y + 1) -' (y9 + 1)))},{((1_. L) . y9)}} is non empty set
the multF of L . [((1_. L) . y9),(x . ((y + 1) -' (y9 + 1)))] is set
0. L is V54(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(0. L) * (x . ((y + 1) -' (y9 + 1))) is Element of the carrier of L
the multF of L . ((0. L),(x . ((y + 1) -' (y9 + 1)))) is Element of the carrier of L
[(0. L),(x . ((y + 1) -' (y9 + 1)))] is set
{(0. L),(x . ((y + 1) -' (y9 + 1)))} is non empty set
{(0. L)} is non empty set
{{(0. L),(x . ((y + 1) -' (y9 + 1)))},{(0. L)}} is non empty set
the multF of L . [(0. L),(x . ((y + 1) -' (y9 + 1)))] is set
Sum (Del (y1,1)) is Element of the carrier of L
y1 . 1 is set
<*(y1 . 1)*> is Relation-like NAT -defined Function-like non empty V31() V38(1) FinSequence-like FinSubsequence-like set
<*(y1 . 1)*> ^ (Del (y1,1)) is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set
y1 /. 1 is Element of the carrier of L
<*(y1 /. 1)*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty V31() V38(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L
<*(y1 /. 1)*> ^ (Del (y1,1)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum <*(y1 /. 1)*> is Element of the carrier of L
(Sum <*(y1 /. 1)*>) + (Sum (Del (y1,1))) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) associative Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the addF of L . ((Sum <*(y1 /. 1)*>),(Sum (Del (y1,1)))) is Element of the carrier of L
[(Sum <*(y1 /. 1)*>),(Sum (Del (y1,1)))] is set
{(Sum <*(y1 /. 1)*>),(Sum (Del (y1,1)))} is non empty set
{(Sum <*(y1 /. 1)*>)} is non empty set
{{(Sum <*(y1 /. 1)*>),(Sum (Del (y1,1)))},{(Sum <*(y1 /. 1)*>)}} is non empty set
the addF of L . [(Sum <*(y1 /. 1)*>),(Sum (Del (y1,1)))] is set
(y1 /. 1) + (Sum (Del (y1,1))) is Element of the carrier of L
the addF of L . ((y1 /. 1),(Sum (Del (y1,1)))) is Element of the carrier of L
[(y1 /. 1),(Sum (Del (y1,1)))] is set
{(y1 /. 1),(Sum (Del (y1,1)))} is non empty set
{(y1 /. 1)} is non empty set
{{(y1 /. 1),(Sum (Del (y1,1)))},{(y1 /. 1)}} is non empty set
the addF of L . [(y1 /. 1),(Sum (Del (y1,1)))] is set
1 -' 1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
(1_. L) . (1 -' 1) is Element of the carrier of L
(y + 1) -' 1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
x . ((y + 1) -' 1) is Element of the carrier of L
((1_. L) . (1 -' 1)) * (x . ((y + 1) -' 1)) is Element of the carrier of L
the multF of L . (((1_. L) . (1 -' 1)),(x . ((y + 1) -' 1))) is Element of the carrier of L
[((1_. L) . (1 -' 1)),(x . ((y + 1) -' 1))] is set
{((1_. L) . (1 -' 1)),(x . ((y + 1) -' 1))} is non empty set
{((1_. L) . (1 -' 1))} is non empty set
{{((1_. L) . (1 -' 1)),(x . ((y + 1) -' 1))},{((1_. L) . (1 -' 1))}} is non empty set
the multF of L . [((1_. L) . (1 -' 1)),(x . ((y + 1) -' 1))] is set
x . y is Element of the carrier of L
((1_. L) . (1 -' 1)) * (x . y) is Element of the carrier of L
the multF of L . (((1_. L) . (1 -' 1)),(x . y)) is Element of the carrier of L
[((1_. L) . (1 -' 1)),(x . y)] is set
{((1_. L) . (1 -' 1)),(x . y)} is non empty set
{{((1_. L) . (1 -' 1)),(x . y)},{((1_. L) . (1 -' 1))}} is non empty set
the multF of L . [((1_. L) . (1 -' 1)),(x . y)] is set
(1_. L) . 0 is Element of the carrier of L
((1_. L) . 0) * (x . y) is Element of the carrier of L
the multF of L . (((1_. L) . 0),(x . y)) is Element of the carrier of L
[((1_. L) . 0),(x . y)] is set
{((1_. L) . 0),(x . y)} is non empty set
{((1_. L) . 0)} is non empty set
{{((1_. L) . 0),(x . y)},{((1_. L) . 0)}} is non empty set
the multF of L . [((1_. L) . 0),(x . y)] is set
1_ L is Element of the carrier of L
1. L is Element of the carrier of L
the OneF of L is Element of the carrier of L
(1_ L) * (x . y) is Element of the carrier of L
the multF of L . ((1_ L),(x . y)) is Element of the carrier of L
[(1_ L),(x . y)] is set
{(1_ L),(x . y)} is non empty set
{(1_ L)} is non empty set
{{(1_ L),(x . y)},{(1_ L)}} is non empty set
the multF of L . [(1_ L),(x . y)] is set
L is non empty right_add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y is Element of the carrier of (L)
y1 is Element of the carrier of (L)
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
y * y1 is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the multF of (L) . [y,y1] is set
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 * y is Element of the carrier of (L)
the multF of (L) . (y1,y) is Element of the carrier of (L)
[y1,y] is set
{y1,y} is non empty set
{y1} is non empty set
{{y1,y},{y1}} is non empty set
the multF of (L) . [y1,y] is set
x9 *' y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty right_add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
1. (L) is Element of the carrier of (L)
the OneF of (L) is Element of the carrier of (L)
x * (1. (L)) is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (x,(1. (L))) is Element of the carrier of (L)
[x,(1. (L))] is set
{x,(1. (L))} is non empty set
{x} is non empty set
{{x,(1. (L))},{x}} is non empty set
the multF of (L) . [x,(1. (L))] is set
(1. (L)) * x is Element of the carrier of (L)
the multF of (L) . ((1. (L)),x) is Element of the carrier of (L)
[(1. (L)),x] is set
{(1. (L)),x} is non empty set
{(1. (L))} is non empty set
{{(1. (L)),x},{(1. (L))}} is non empty set
the multF of (L) . [(1. (L)),x] is set
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
(L) is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed Abelian add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (L)
y1 is Element of the carrier of (L)
y + y1 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) commutative associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the addF of (L) . [y,y1] is set
x * (y + y1) is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
the multF of (L) . (x,(y + y1)) is Element of the carrier of (L)
[x,(y + y1)] is set
{x,(y + y1)} is non empty set
{x} is non empty set
{{x,(y + y1)},{x}} is non empty set
the multF of (L) . [x,(y + y1)] is set
x * y is Element of the carrier of (L)
the multF of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the multF of (L) . [x,y] is set
x * y1 is Element of the carrier of (L)
the multF of (L) . (x,y1) is Element of the carrier of (L)
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the multF of (L) . [x,y1] is set
(x * y) + (x * y1) is Element of the carrier of (L)
the addF of (L) . ((x * y),(x * y1)) is Element of the carrier of (L)
[(x * y),(x * y1)] is set
{(x * y),(x * y1)} is non empty set
{(x * y)} is non empty set
{{(x * y),(x * y1)},{(x * y)}} is non empty set
the addF of (L) . [(x * y),(x * y1)] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 *' p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y + y1 is Element of the carrier of (L)
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * (y + y1) is Element of the carrier of (L)
the multF of (L) . (x,(y + y1)) is Element of the carrier of (L)
[x,(y + y1)] is set
{x,(y + y1)} is non empty set
{{x,(y + y1)},{x}} is non empty set
the multF of (L) . [x,(y + y1)] is set
y9 *' (x9 + p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y9 *' x9) + (y9 *' p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * y) + (x * y1) is Element of the carrier of (L)
the carrier of (L) is non empty set
y is Element of the carrier of (L)
y1 is Element of the carrier of (L)
y + y1 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) commutative associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the addF of (L) . [y,y1] is set
x is Element of the carrier of (L)
(y + y1) * x is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
the multF of (L) . ((y + y1),x) is Element of the carrier of (L)
[(y + y1),x] is set
{(y + y1),x} is non empty set
{(y + y1)} is non empty set
{{(y + y1),x},{(y + y1)}} is non empty set
the multF of (L) . [(y + y1),x] is set
y * x is Element of the carrier of (L)
the multF of (L) . (y,x) is Element of the carrier of (L)
[y,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
the multF of (L) . [y,x] is set
y1 * x is Element of the carrier of (L)
the multF of (L) . (y1,x) is Element of the carrier of (L)
[y1,x] is set
{y1,x} is non empty set
{y1} is non empty set
{{y1,x},{y1}} is non empty set
the multF of (L) . [y1,x] is set
(y * x) + (y1 * x) is Element of the carrier of (L)
the addF of (L) . ((y * x),(y1 * x)) is Element of the carrier of (L)
[(y * x),(y1 * x)] is set
{(y * x),(y1 * x)} is non empty set
{(y * x)} is non empty set
{{(y * x),(y1 * x)},{(y * x)}} is non empty set
the addF of (L) . [(y * x),(y1 * x)] is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x9 *' y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p *' y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y + y1 is Element of the carrier of (L)
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y + y1) * x is Element of the carrier of (L)
the multF of (L) . ((y + y1),x) is Element of the carrier of (L)
[(y + y1),x] is set
{(y + y1),x} is non empty set
{(y + y1)} is non empty set
{{(y + y1),x},{(y + y1)}} is non empty set
the multF of (L) . [(y + y1),x] is set
(x9 + p) *' y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x9 *' y9) + (p *' y9) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y * x) + (y1 * x) is Element of the carrier of (L)
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x is Element of the carrier of L
y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y + y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * (y + y1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * y) + (x * y1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
(x * (y + y1)) . y9 is Element of the carrier of L
((x * y) + (x * y1)) . y9 is Element of the carrier of L
(y + y1) . y9 is Element of the carrier of L
x * ((y + y1) . y9) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,((y + y1) . y9)) is Element of the carrier of L
[x,((y + y1) . y9)] is set
{x,((y + y1) . y9)} is non empty set
{x} is non empty set
{{x,((y + y1) . y9)},{x}} is non empty set
the multF of L . [x,((y + y1) . y9)] is set
y . y9 is Element of the carrier of L
y1 . y9 is Element of the carrier of L
(y . y9) + (y1 . y9) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the addF of L . ((y . y9),(y1 . y9)) is Element of the carrier of L
[(y . y9),(y1 . y9)] is set
{(y . y9),(y1 . y9)} is non empty set
{(y . y9)} is non empty set
{{(y . y9),(y1 . y9)},{(y . y9)}} is non empty set
the addF of L . [(y . y9),(y1 . y9)] is set
x * ((y . y9) + (y1 . y9)) is Element of the carrier of L
the multF of L . (x,((y . y9) + (y1 . y9))) is Element of the carrier of L
[x,((y . y9) + (y1 . y9))] is set
{x,((y . y9) + (y1 . y9))} is non empty set
{{x,((y . y9) + (y1 . y9))},{x}} is non empty set
the multF of L . [x,((y . y9) + (y1 . y9))] is set
x * (y . y9) is Element of the carrier of L
the multF of L . (x,(y . y9)) is Element of the carrier of L
[x,(y . y9)] is set
{x,(y . y9)} is non empty set
{{x,(y . y9)},{x}} is non empty set
the multF of L . [x,(y . y9)] is set
x * (y1 . y9) is Element of the carrier of L
the multF of L . (x,(y1 . y9)) is Element of the carrier of L
[x,(y1 . y9)] is set
{x,(y1 . y9)} is non empty set
{{x,(y1 . y9)},{x}} is non empty set
the multF of L . [x,(y1 . y9)] is set
(x * (y . y9)) + (x * (y1 . y9)) is Element of the carrier of L
the addF of L . ((x * (y . y9)),(x * (y1 . y9))) is Element of the carrier of L
[(x * (y . y9)),(x * (y1 . y9))] is set
{(x * (y . y9)),(x * (y1 . y9))} is non empty set
{(x * (y . y9))} is non empty set
{{(x * (y . y9)),(x * (y1 . y9))},{(x * (y . y9))}} is non empty set
the addF of L . [(x * (y . y9)),(x * (y1 . y9))] is set
(x * y) . y9 is Element of the carrier of L
((x * y) . y9) + (x * (y1 . y9)) is Element of the carrier of L
the addF of L . (((x * y) . y9),(x * (y1 . y9))) is Element of the carrier of L
[((x * y) . y9),(x * (y1 . y9))] is set
{((x * y) . y9),(x * (y1 . y9))} is non empty set
{((x * y) . y9)} is non empty set
{{((x * y) . y9),(x * (y1 . y9))},{((x * y) . y9)}} is non empty set
the addF of L . [((x * y) . y9),(x * (y1 . y9))] is set
(x * y1) . y9 is Element of the carrier of L
((x * y) . y9) + ((x * y1) . y9) is Element of the carrier of L
the addF of L . (((x * y) . y9),((x * y1) . y9)) is Element of the carrier of L
[((x * y) . y9),((x * y1) . y9)] is set
{((x * y) . y9),((x * y1) . y9)} is non empty set
{{((x * y) . y9),((x * y1) . y9)},{((x * y) . y9)}} is non empty set
the addF of L . [((x * y) . y9),((x * y1) . y9)] is set
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x + y is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,y) is Element of the carrier of L
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of L . [x,y] is set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x + y) * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * y1) + (y * y1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
((x + y) * y1) . y9 is Element of the carrier of L
((x * y1) + (y * y1)) . y9 is Element of the carrier of L
y1 . y9 is Element of the carrier of L
(x + y) * (y1 . y9) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((x + y),(y1 . y9)) is Element of the carrier of L
[(x + y),(y1 . y9)] is set
{(x + y),(y1 . y9)} is non empty set
{(x + y)} is non empty set
{{(x + y),(y1 . y9)},{(x + y)}} is non empty set
the multF of L . [(x + y),(y1 . y9)] is set
x * (y1 . y9) is Element of the carrier of L
the multF of L . (x,(y1 . y9)) is Element of the carrier of L
[x,(y1 . y9)] is set
{x,(y1 . y9)} is non empty set
{{x,(y1 . y9)},{x}} is non empty set
the multF of L . [x,(y1 . y9)] is set
y * (y1 . y9) is Element of the carrier of L
the multF of L . (y,(y1 . y9)) is Element of the carrier of L
[y,(y1 . y9)] is set
{y,(y1 . y9)} is non empty set
{y} is non empty set
{{y,(y1 . y9)},{y}} is non empty set
the multF of L . [y,(y1 . y9)] is set
(x * (y1 . y9)) + (y * (y1 . y9)) is Element of the carrier of L
the addF of L . ((x * (y1 . y9)),(y * (y1 . y9))) is Element of the carrier of L
[(x * (y1 . y9)),(y * (y1 . y9))] is set
{(x * (y1 . y9)),(y * (y1 . y9))} is non empty set
{(x * (y1 . y9))} is non empty set
{{(x * (y1 . y9)),(y * (y1 . y9))},{(x * (y1 . y9))}} is non empty set
the addF of L . [(x * (y1 . y9)),(y * (y1 . y9))] is set
(x * y1) . y9 is Element of the carrier of L
((x * y1) . y9) + (y * (y1 . y9)) is Element of the carrier of L
the addF of L . (((x * y1) . y9),(y * (y1 . y9))) is Element of the carrier of L
[((x * y1) . y9),(y * (y1 . y9))] is set
{((x * y1) . y9),(y * (y1 . y9))} is non empty set
{((x * y1) . y9)} is non empty set
{{((x * y1) . y9),(y * (y1 . y9))},{((x * y1) . y9)}} is non empty set
the addF of L . [((x * y1) . y9),(y * (y1 . y9))] is set
(y * y1) . y9 is Element of the carrier of L
((x * y1) . y9) + ((y * y1) . y9) is Element of the carrier of L
the addF of L . (((x * y1) . y9),((y * y1) . y9)) is Element of the carrier of L
[((x * y1) . y9),((y * y1) . y9)] is set
{((x * y1) . y9),((y * y1) . y9)} is non empty set
{{((x * y1) . y9),((y * y1) . y9)},{((x * y1) . y9)}} is non empty set
the addF of L . [((x * y1) . y9),((y * y1) . y9)] is set
L is non empty associative doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
x * y is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,y) is Element of the carrier of L
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * y) * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * (y * y1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
((x * y) * y1) . y9 is Element of the carrier of L
(x * (y * y1)) . y9 is Element of the carrier of L
y1 . y9 is Element of the carrier of L
(x * y) * (y1 . y9) is Element of the carrier of L
the multF of L . ((x * y),(y1 . y9)) is Element of the carrier of L
[(x * y),(y1 . y9)] is set
{(x * y),(y1 . y9)} is non empty set
{(x * y)} is non empty set
{{(x * y),(y1 . y9)},{(x * y)}} is non empty set
the multF of L . [(x * y),(y1 . y9)] is set
y * (y1 . y9) is Element of the carrier of L
the multF of L . (y,(y1 . y9)) is Element of the carrier of L
[y,(y1 . y9)] is set
{y,(y1 . y9)} is non empty set
{y} is non empty set
{{y,(y1 . y9)},{y}} is non empty set
the multF of L . [y,(y1 . y9)] is set
x * (y * (y1 . y9)) is Element of the carrier of L
the multF of L . (x,(y * (y1 . y9))) is Element of the carrier of L
[x,(y * (y1 . y9))] is set
{x,(y * (y1 . y9))} is non empty set
{{x,(y * (y1 . y9))},{x}} is non empty set
the multF of L . [x,(y * (y1 . y9))] is set
(y * y1) . y9 is Element of the carrier of L
x * ((y * y1) . y9) is Element of the carrier of L
the multF of L . (x,((y * y1) . y9)) is Element of the carrier of L
[x,((y * y1) . y9)] is set
{x,((y * y1) . y9)} is non empty set
{{x,((y * y1) . y9)},{x}} is non empty set
the multF of L . [x,((y * y1) . y9)] is set
L is non empty unital associative right_unital well-unital left_unital doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
1. L is Element of the carrier of L
the OneF of L is Element of the carrier of L
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(1. L) * x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
((1. L) * x) . y is Element of the carrier of L
x . y is Element of the carrier of L
(1. L) * (x . y) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((1. L),(x . y)) is Element of the carrier of L
[(1. L),(x . y)] is set
{(1. L),(x . y)} is non empty set
{(1. L)} is non empty set
{{(1. L),(x . y)},{(1. L)}} is non empty set
the multF of L . [(1. L),(x . y)] is set
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(L) is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed (L) (L)
the carrier of L is non empty set
the carrier of (L) is non empty set
y is Element of the carrier of L
y1 is Element of the carrier of (L)
y9 is Element of the carrier of (L)
y1 + y9 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) commutative associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the addF of (L) . [y1,y9] is set
y * (y1 + y9) is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . (y,(y1 + y9)) is Element of the carrier of (L)
[y,(y1 + y9)] is set
{y,(y1 + y9)} is non empty set
{y} is non empty set
{{y,(y1 + y9)},{y}} is non empty set
the lmult of (L) . [y,(y1 + y9)] is set
y * y1 is Element of the carrier of (L)
the lmult of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{{y,y1},{y}} is non empty set
the lmult of (L) . [y,y1] is set
y * y9 is Element of the carrier of (L)
the lmult of (L) . (y,y9) is Element of the carrier of (L)
[y,y9] is set
{y,y9} is non empty set
{{y,y9},{y}} is non empty set
the lmult of (L) . [y,y9] is set
(y * y1) + (y * y9) is Element of the carrier of (L)
the addF of (L) . ((y * y1),(y * y9)) is Element of the carrier of (L)
[(y * y1),(y * y9)] is set
{(y * y1),(y * y9)} is non empty set
{(y * y1)} is non empty set
{{(y * y1),(y * y9)},{(y * y1)}} is non empty set
the addF of (L) . [(y * y1),(y * y9)] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y1 + y9 is Element of the carrier of (L)
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
q is Element of the carrier of (L)
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * q is Element of the carrier of (L)
the lmult of (L) . (y,q) is Element of the carrier of (L)
[y,q] is set
{y,q} is non empty set
{{y,q},{y}} is non empty set
the lmult of (L) . [y,q] is set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * (y1 + y9) is Element of the carrier of (L)
the lmult of (L) . (y,(y1 + y9)) is Element of the carrier of (L)
[y,(y1 + y9)] is set
{y,(y1 + y9)} is non empty set
{{y,(y1 + y9)},{y}} is non empty set
the lmult of (L) . [y,(y1 + y9)] is set
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * (x9 + p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Element of the carrier of L
x1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 * p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x1 * x9) + (x1 * p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y * y1) + (y * y9) is Element of the carrier of (L)
the carrier of L is non empty set
the carrier of (L) is non empty set
y is Element of the carrier of L
y1 is Element of the carrier of L
y + y1 is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) commutative associative Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (y,y1) is Element of the carrier of L
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the addF of L . [y,y1] is set
y9 is Element of the carrier of (L)
(y + y1) * y9 is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . ((y + y1),y9) is Element of the carrier of (L)
[(y + y1),y9] is set
{(y + y1),y9} is non empty set
{(y + y1)} is non empty set
{{(y + y1),y9},{(y + y1)}} is non empty set
the lmult of (L) . [(y + y1),y9] is set
y * y9 is Element of the carrier of (L)
the lmult of (L) . (y,y9) is Element of the carrier of (L)
[y,y9] is set
{y,y9} is non empty set
{{y,y9},{y}} is non empty set
the lmult of (L) . [y,y9] is set
y1 * y9 is Element of the carrier of (L)
the lmult of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the lmult of (L) . [y1,y9] is set
(y * y9) + (y1 * y9) is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) commutative associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . ((y * y9),(y1 * y9)) is Element of the carrier of (L)
[(y * y9),(y1 * y9)] is set
{(y * y9),(y1 * y9)} is non empty set
{(y * y9)} is non empty set
{{(y * y9),(y1 * y9)},{(y * y9)}} is non empty set
the addF of (L) . [(y * y9),(y1 * y9)] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y + y1 is Element of the carrier of L
(y + y1) * y9 is Element of the carrier of (L)
the lmult of (L) . ((y + y1),y9) is Element of the carrier of (L)
[(y + y1),y9] is set
{(y + y1),y9} is non empty set
{(y + y1)} is non empty set
{{(y + y1),y9},{(y + y1)}} is non empty set
the lmult of (L) . [(y + y1),y9] is set
p is Element of the carrier of L
x1 is Element of the carrier of L
p + x1 is Element of the carrier of L
the addF of L . (p,x1) is Element of the carrier of L
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the addF of L . [p,x1] is set
(p + x1) * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(p * x9) + (x1 * x9) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(y * y9) + (y1 * y9) is Element of the carrier of (L)
the carrier of L is non empty set
the carrier of (L) is non empty set
y is Element of the carrier of L
y1 is Element of the carrier of L
y * y1 is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (y,y1) is Element of the carrier of L
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the multF of L . [y,y1] is set
y9 is Element of the carrier of (L)
(y * y1) * y9 is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . ((y * y1),y9) is Element of the carrier of (L)
[(y * y1),y9] is set
{(y * y1),y9} is non empty set
{(y * y1)} is non empty set
{{(y * y1),y9},{(y * y1)}} is non empty set
the lmult of (L) . [(y * y1),y9] is set
y1 * y9 is Element of the carrier of (L)
the lmult of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the lmult of (L) . [y1,y9] is set
y * (y1 * y9) is Element of the carrier of (L)
the lmult of (L) . (y,(y1 * y9)) is Element of the carrier of (L)
[y,(y1 * y9)] is set
{y,(y1 * y9)} is non empty set
{{y,(y1 * y9)},{y}} is non empty set
the lmult of (L) . [y,(y1 * y9)] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p is Element of the carrier of L
x1 is Element of the carrier of L
p * x1 is Element of the carrier of L
the multF of L . (p,x1) is Element of the carrier of L
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
the multF of L . [p,x1] is set
(p * x1) * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p * (x1 * x9) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
the carrier of (L) is non empty set
1. L is Element of the carrier of L
the carrier of L is non empty set
the OneF of L is Element of the carrier of L
y is Element of the carrier of (L)
(1. L) * y is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . ((1. L),y) is Element of the carrier of (L)
[(1. L),y] is set
{(1. L),y} is non empty set
{(1. L)} is non empty set
{{(1. L),y},{(1. L)}} is non empty set
the lmult of (L) . [(1. L),y] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(1. L) * y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed associative right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x is Element of the carrier of L
y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y *' y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * (y *' y1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * y is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * y) *' y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
y9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
(x * (y *' y1)) . y9 is Element of the carrier of L
((x * y) *' y1) . y9 is Element of the carrier of L
y9 + 1 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative set
(y *' y1) . y9 is Element of the carrier of L
x9 is Relation-like NAT -defined the carrier of L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len x9 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
Sum x9 is Element of the carrier of L
dom x9 is Element of bool NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len p is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
Sum p is Element of the carrier of L
dom p is Element of bool NAT
x * x9 is Relation-like NAT -defined the carrier of L -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
dom (x * x9) is Element of bool NAT
x1 is V24() V25() V26() V30() V42() V43() ext-real non negative set
p . x1 is set
(x * x9) . x1 is set
x1 -' 1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y . (x1 -' 1) is Element of the carrier of L
(y9 + 1) -' x1 is V24() V25() V26() V30() V42() V43() ext-real non negative Element of NAT
y1 . ((y9 + 1) -' x1) is Element of the carrier of L
(y . (x1 -' 1)) * (y1 . ((y9 + 1) -' x1)) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((y . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))) is Element of the carrier of L
[(y . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))] is set
{(y . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))} is non empty set
{(y . (x1 -' 1))} is non empty set
{{(y . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))},{(y . (x1 -' 1))}} is non empty set
the multF of L . [(y . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))] is set
x9 . x1 is set
x9 /. x1 is Element of the carrier of L
(x * y) . (x1 -' 1) is Element of the carrier of L
((x * y) . (x1 -' 1)) * (y1 . ((y9 + 1) -' x1)) is Element of the carrier of L
the multF of L . (((x * y) . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))) is Element of the carrier of L
[((x * y) . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))] is set
{((x * y) . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))} is non empty set
{((x * y) . (x1 -' 1))} is non empty set
{{((x * y) . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))},{((x * y) . (x1 -' 1))}} is non empty set
the multF of L . [((x * y) . (x1 -' 1)),(y1 . ((y9 + 1) -' x1))] is set
x * (y . (x1 -' 1)) is Element of the carrier of L
the multF of L . (x,(y . (x1 -' 1))) is Element of the carrier of L
[x,(y . (x1 -' 1))] is set
{x,(y . (x1 -' 1))} is non empty set
{x} is non empty set
{{x,(y . (x1 -' 1))},{x}} is non empty set
the multF of L . [x,(y . (x1 -' 1))] is set
(x * (y . (x1 -' 1))) * (y1 . ((y9 + 1) -' x1)) is Element of the carrier of L
the multF of L . ((x * (y . (x1 -' 1))),(y1 . ((y9 + 1) -' x1))) is Element of the carrier of L
[(x * (y . (x1 -' 1))),(y1 . ((y9 + 1) -' x1))] is set
{(x * (y . (x1 -' 1))),(y1 . ((y9 + 1) -' x1))} is non empty set
{(x * (y . (x1 -' 1)))} is non empty set
{{(x * (y . (x1 -' 1))),(y1 . ((y9 + 1) -' x1))},{(x * (y . (x1 -' 1)))}} is non empty set
the multF of L . [(x * (y . (x1 -' 1))),(y1 . ((y9 + 1) -' x1))] is set
x * (x9 /. x1) is Element of the carrier of L
the multF of L . (x,(x9 /. x1)) is Element of the carrier of L
[x,(x9 /. x1)] is set
{x,(x9 /. x1)} is non empty set
{{x,(x9 /. x1)},{x}} is non empty set
the multF of L . [x,(x9 /. x1)] is set
(x * x9) /. x1 is Element of the carrier of L
x * (Sum x9) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(Sum x9)) is Element of the carrier of L
[x,(Sum x9)] is set
{x,(Sum x9)} is non empty set
{x} is non empty set
{{x,(Sum x9)},{x}} is non empty set
the multF of L . [x,(Sum x9)] is set
Sum (x * x9) is Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed associative right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
(L) is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed right-distributive left-distributive distributive Abelian add-associative right_zeroed (L) (L)
the carrier of L is non empty set
the carrier of (L) is non empty set
x is Element of the carrier of L
y is Element of the carrier of (L)
y1 is Element of the carrier of (L)
y * y1 is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (y,y1) is Element of the carrier of (L)
[y,y1] is set
{y,y1} is non empty set
{y} is non empty set
{{y,y1},{y}} is non empty set
the multF of (L) . [y,y1] is set
x * (y * y1) is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . (x,(y * y1)) is Element of the carrier of (L)
[x,(y * y1)] is set
{x,(y * y1)} is non empty set
{x} is non empty set
{{x,(y * y1)},{x}} is non empty set
the lmult of (L) . [x,(y * y1)] is set
x * y is Element of the carrier of (L)
the lmult of (L) . (x,y) is Element of the carrier of (L)
[x,y] is set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the lmult of (L) . [x,y] is set
(x * y) * y1 is Element of the carrier of (L)
the multF of (L) . ((x * y),y1) is Element of the carrier of (L)
[(x * y),y1] is set
{(x * y),y1} is non empty set
{(x * y)} is non empty set
{{(x * y),y1},{(x * y)}} is non empty set
the multF of (L) . [(x * y),y1] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
y9 is Element of the carrier of (L)
x9 is Element of the carrier of (L)
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
p *' x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
x * (p *' x1) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
(x * p) *' x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]
L is 1-sorted
x is (L)
the carrier of x is set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the addF of x || the carrier of x is Relation-like Function-like set
the addF of x | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
the multF of x || the carrier of x is Relation-like Function-like set
the multF of x | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
the lmult of x | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
L is 1-sorted
x is (L)
the carrier of x is set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x || the carrier of x is Relation-like Function-like set
the addF of x | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the multF of x || the carrier of x is Relation-like Function-like set
the multF of x | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
L is 1-sorted
x is (L)
y is (L)
y1 is (L)
the carrier of x is set
the carrier of y is set
[: the carrier of x, the carrier of x:] is Relation-like set
[: the carrier of y, the carrier of y:] is Relation-like set
the carrier of y1 is set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
1. y1 is Element of the carrier of y1
the OneF of y1 is Element of the carrier of y1
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
0. y1 is V54(y1) Element of the carrier of y1
the ZeroF of y1 is Element of the carrier of y1
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of y1 is Relation-like [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued Function-like V18([: the carrier of y1, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:]
[: the carrier of y1, the carrier of y1:] is Relation-like set
[:[: the carrier of y1, the carrier of y1:], the carrier of y1:] is Relation-like set
bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:] is non empty set
the addF of y1 || the carrier of x is Relation-like Function-like set
the addF of y1 | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the multF of y1 is Relation-like [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued Function-like V18([: the carrier of y1, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:]
the multF of y1 || the carrier of x is Relation-like Function-like set
the multF of y1 | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued set
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
[: the carrier of L, the carrier of y1:] is Relation-like set
the lmult of y1 is Relation-like [: the carrier of L, the carrier of y1:] -defined the carrier of y1 -valued Function-like V18([: the carrier of L, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:]
[:[: the carrier of L, the carrier of y1:], the carrier of y1:] is Relation-like set
bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:] is non empty set
the lmult of y1 | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y1:] -defined the carrier of y1 -valued Function-like Element of bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:]
1. y is Element of the carrier of y
the OneF of y is Element of the carrier of y
0. y is V54(y) Element of the carrier of y
the ZeroF of y is Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the addF of y || the carrier of x is Relation-like Function-like set
the addF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
the addF of y1 || the carrier of y is Relation-like Function-like set
the addF of y1 | [: the carrier of y, the carrier of y:] is Relation-like [: the carrier of y, the carrier of y:] -defined [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued set
( the addF of y1 || the carrier of y) || the carrier of x is Relation-like Function-like set
( the addF of y1 || the carrier of y) | [: the carrier of x, the carrier of x:] is Relation-like set
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
the multF of y || the carrier of x is Relation-like Function-like set
the multF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
the multF of y1 || the carrier of y is Relation-like Function-like set
the multF of y1 | [: the carrier of y, the carrier of y:] is Relation-like [: the carrier of y, the carrier of y:] -defined [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued set
( the multF of y1 || the carrier of y) || the carrier of x is Relation-like Function-like set
( the multF of y1 || the carrier of y) | [: the carrier of x, the carrier of x:] is Relation-like set
[: the carrier of L, the carrier of y:] is Relation-like set
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
the lmult of y | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
the lmult of y1 | [: the carrier of L, the carrier of y:] is Relation-like [: the carrier of L, the carrier of y1:] -defined [: the carrier of L, the carrier of y:] -defined [: the carrier of L, the carrier of y1:] -defined the carrier of y1 -valued Function-like Element of bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:]
( the lmult of y1 | [: the carrier of L, the carrier of y:]) | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y1:] -defined the carrier of y1 -valued Function-like Element of bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:]
L is 1-sorted
x is (L)
y is (L)
the carrier of x is set
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the ZeroF of x is Element of the carrier of x
the OneF of x is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
(L, the carrier of x, the addF of x, the multF of x, the ZeroF of x, the OneF of x, the lmult of x) is (L) (L)
the carrier of y is set
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
the ZeroF of y is Element of the carrier of y
the OneF of y is Element of the carrier of y
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[: the carrier of L, the carrier of y:] is Relation-like set
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
(L, the carrier of y, the addF of y, the multF of y, the ZeroF of y, the OneF of y, the lmult of y) is (L) (L)
dom the lmult of y is Relation-like set
the lmult of y | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
dom the addF of y is Relation-like set
0. x is V54(x) Element of the carrier of x
0. y is V54(y) Element of the carrier of y
1. x is Element of the carrier of x
1. y is Element of the carrier of y
dom the multF of y is Relation-like set
the multF of y || the carrier of x is Relation-like Function-like set
the multF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
the addF of y || the carrier of x is Relation-like Function-like set
the addF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
L is 1-sorted
x is (L)
the carrier of x is set
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the ZeroF of x is Element of the carrier of x
the OneF of x is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
(L, the carrier of x, the addF of x, the multF of x, the ZeroF of x, the OneF of x, the lmult of x) is (L) (L)
y is (L)
the carrier of y is set
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
the ZeroF of y is Element of the carrier of y
the OneF of y is Element of the carrier of y
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[: the carrier of L, the carrier of y:] is Relation-like set
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
(L, the carrier of y, the addF of y, the multF of y, the ZeroF of y, the OneF of y, the lmult of y) is (L) (L)
1. x is Element of the carrier of x
1. y is Element of the carrier of y
0. x is V54(x) Element of the carrier of x
0. y is V54(y) Element of the carrier of y
the addF of y || the carrier of x is Relation-like Function-like set
the addF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
the multF of y || the carrier of x is Relation-like Function-like set
the multF of y | [: the carrier of x, the carrier of x:] is Relation-like [: the carrier of x, the carrier of x:] -defined [: the carrier of y, the carrier of y:] -defined the carrier of y -valued set
the lmult of y | [: the carrier of L, the carrier of x:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
dom the addF of y is Relation-like set
dom the multF of y is Relation-like set
dom the lmult of y is Relation-like set
L is non empty 1-sorted
{0} is non empty set
the carrier of L is non empty set
[: the carrier of L,{0}:] is Relation-like non empty set
[:[: the carrier of L,{0}:],{0}:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],{0}:] is non empty set
[: the carrier of L,{0}:] --> 0 is Relation-like [: the carrier of L,{0}:] -defined NAT -valued Function-like non empty total V18([: the carrier of L,{0}:], NAT ) Element of bool [:[: the carrier of L,{0}:],NAT:]
[:[: the carrier of L,{0}:],NAT:] is Relation-like non empty set
bool [:[: the carrier of L,{0}:],NAT:] is non empty set
[:{0},{0}:] is Relation-like non empty set
[:[:{0},{0}:],{0}:] is Relation-like non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]
y is Element of {0}
x is Relation-like [: the carrier of L,{0}:] -defined {0} -valued Function-like non empty total V18([: the carrier of L,{0}:],{0}) Element of bool [:[: the carrier of L,{0}:],{0}:]
(L,{0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:], the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:],y,y,x) is (L) (L)
x9 is (L) (L)
L is 1-sorted
x is (L)
the carrier of x is set
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is set
[: the carrier of L, the carrier of x:] is Relation-like set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
(L, the carrier of x, the addF of x, the multF of x,(0. x),(1. x), the lmult of x) is (L) (L)
y is (L,x)
L is non empty 1-sorted
x is non empty (L)
the carrier of x is non empty set
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
the carrier of L is non empty set
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
(L, the carrier of x, the addF of x, the multF of x,(0. x),(1. x), the lmult of x) is (L) (L)
y is (L,x)
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
y is non empty (L,x)
the carrier of y is non empty set
y1 is Element of the carrier of x
y9 is Element of the carrier of x
y1 + y9 is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . (y1,y9) is Element of the carrier of x
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the addF of x . [y1,y9] is set
x9 is Element of the carrier of y
p is Element of the carrier of y
x9 + p is Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the addF of y . (x9,p) is Element of the carrier of y
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the addF of y . [x9,p] is set
the addF of x || the carrier of y is Relation-like Function-like set
the addF of x | [: the carrier of y, the carrier of y:] is Relation-like [: the carrier of y, the carrier of y:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
( the addF of x || the carrier of y) . [x9,p] is set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
y is non empty (L,x)
the carrier of y is non empty set
y1 is Element of the carrier of x
y9 is Element of the carrier of x
y1 * y9 is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (y1,y9) is Element of the carrier of x
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the multF of x . [y1,y9] is set
x9 is Element of the carrier of y
p is Element of the carrier of y
x9 * p is Element of the carrier of y
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the multF of y . (x9,p) is Element of the carrier of y
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the multF of y . [x9,p] is set
the multF of x || the carrier of y is Relation-like Function-like set
the multF of x | [: the carrier of y, the carrier of y:] is Relation-like [: the carrier of y, the carrier of y:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
( the multF of x || the carrier of y) . [x9,p] is set
L is non empty multMagma
the carrier of L is non empty set
x is non empty (L)
the carrier of x is non empty set
y is non empty (L,x)
the carrier of y is non empty set
y1 is Element of the carrier of L
y9 is Element of the carrier of x
y1 * y9 is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x . (y1,y9) is Element of the carrier of x
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the lmult of x . [y1,y9] is set
x9 is Element of the carrier of y
y1 * x9 is Element of the carrier of y
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[: the carrier of L, the carrier of y:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
the lmult of y . (y1,x9) is Element of the carrier of y
[y1,x9] is set
{y1,x9} is non empty set
{{y1,x9},{y1}} is non empty set
the lmult of y . [y1,x9] is set
the lmult of x | [: the carrier of L, the carrier of y:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L, the carrier of y:] -defined [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
( the lmult of x | [: the carrier of L, the carrier of y:]) . [y1,x9] is set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
y is non empty (L,x)
the carrier of y is non empty set
y1 is non empty set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
1. y is Element of the carrier of y
the OneF of y is Element of the carrier of y
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
0. y is V54(y) Element of the carrier of y
the ZeroF of y is Element of the carrier of y
the carrier of L is non empty set
y9 is Element of bool the carrier of x
x9 is Element of the carrier of L
p is Element of the carrier of x
x9 * p is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x . (x9,p) is Element of the carrier of x
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the lmult of x . [x9,p] is set
x1 is Element of the carrier of y
x9 * x1 is Element of the carrier of y
the lmult of y is Relation-like [: the carrier of L, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of L, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of L, the carrier of y:], the carrier of y:]
[: the carrier of L, the carrier of y:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y:], the carrier of y:] is non empty set
the lmult of y . (x9,x1) is Element of the carrier of y
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the lmult of y . [x9,x1] is set
x9 is Element of the carrier of x
p is Element of the carrier of x
x9 * p is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (x9,p) is Element of the carrier of x
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the multF of x . [x9,p] is set
x1 is Element of the carrier of x
q is Element of the carrier of x
x9 is Element of the carrier of y
y9 is Element of the carrier of y
x9 * y9 is Element of the carrier of y
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the multF of y . (x9,y9) is Element of the carrier of y
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
the multF of y . [x9,y9] is set
x9 is Element of the carrier of x
p is Element of the carrier of x
x9 + p is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . (x9,p) is Element of the carrier of x
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the addF of x . [x9,p] is set
q is Element of the carrier of y
x1 is Element of the carrier of y
q + x1 is Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like non empty total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the addF of y . (q,x1) is Element of the carrier of y
[q,x1] is set
{q,x1} is non empty set
{q} is non empty set
{{q,x1},{q}} is non empty set
the addF of y . [q,x1] is set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
y is Element of bool the carrier of x
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
the carrier of L is non empty set
[: the carrier of L, the carrier of x:] is Relation-like non empty set
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
[: the carrier of L,y:] is Relation-like set
the lmult of x | [: the carrier of L,y:] is Relation-like [: the carrier of L, the carrier of x:] -defined [: the carrier of L,y:] -defined [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
y9 is Relation-like Function-like set
x9 is set
y9 . x9 is set
p is set
x1 is set
[p,x1] is set
{p,x1} is non empty set
{p} is non empty set
{{p,x1},{p}} is non empty set
x9 is Element of the carrier of L
q is Element of the carrier of x
x9 * q is Element of the carrier of x
the lmult of x . (x9,q) is Element of the carrier of x
[x9,q] is set
{x9,q} is non empty set
{x9} is non empty set
{{x9,q},{x9}} is non empty set
the lmult of x . [x9,q] is set
dom the lmult of x is Relation-like non empty set
dom y9 is set
[:[: the carrier of L,y:],y:] is Relation-like set
bool [:[: the carrier of L,y:],y:] is non empty set
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x || y is Relation-like Function-like set
[:y,y:] is Relation-like set
the addF of x | [:y,y:] is Relation-like [:y,y:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the multF of x || y is Relation-like Function-like set
the multF of x | [:y,y:] is Relation-like [:y,y:] -defined [: the carrier of x, the carrier of x:] -defined the carrier of x -valued set
x1 is Relation-like Function-like set
q is set
x1 . q is set
x9 is set
y9 is set
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
x1 is Element of the carrier of x
y1 is Element of the carrier of x
x1 * y1 is Element of the carrier of x
the multF of x . (x1,y1) is Element of the carrier of x
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the multF of x . [x1,y1] is set
dom the multF of x is Relation-like non empty set
dom x1 is set
[:[:y,y:],y:] is Relation-like set
bool [:[:y,y:],y:] is non empty set
p is Relation-like Function-like set
dom p is set
dom the addF of x is Relation-like non empty set
x9 is set
p . x9 is set
y9 is set
x1 is set
[y9,x1] is set
{y9,x1} is non empty set
{y9} is non empty set
{{y9,x1},{y9}} is non empty set
y1 is Element of the carrier of x
c₁₄ is Element of the carrier of x
y1 + c₁₄ is Element of the carrier of x
the addF of x . (y1,c₁₄) is Element of the carrier of x
[y1,c₁₄] is set
{y1,c₁₄} is non empty set
{y1} is non empty set
{{y1,c₁₄},{y1}} is non empty set
the addF of x . [y1,c₁₄] is set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
x9 is Relation-like [:y,y:] -defined y -valued Function-like V18([:y,y:],y) Element of bool [:[:y,y:],y:]
q is Relation-like [:y,y:] -defined y -valued Function-like V18([:y,y:],y) Element of bool [:[:y,y:],y:]
y1 is Element of y
y9 is Element of y
x9 is Relation-like [: the carrier of L,y:] -defined y -valued Function-like V18([: the carrier of L,y:],y) Element of bool [:[: the carrier of L,y:],y:]
(L,y,x9,q,y1,y9,x9) is (L) (L)
1. (L,y,x9,q,y1,y9,x9) is Element of the carrier of (L,y,x9,q,y1,y9,x9)
the carrier of (L,y,x9,q,y1,y9,x9) is set
the OneF of (L,y,x9,q,y1,y9,x9) is Element of the carrier of (L,y,x9,q,y1,y9,x9)
0. (L,y,x9,q,y1,y9,x9) is V54((L,y,x9,q,y1,y9,x9)) Element of the carrier of (L,y,x9,q,y1,y9,x9)
the ZeroF of (L,y,x9,q,y1,y9,x9) is Element of the carrier of (L,y,x9,q,y1,y9,x9)
y1 is (L) (L,x)
the carrier of y1 is set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
y is non empty Element of bool the carrier of x
y1 is Element of bool (bool the carrier of x)
meet y1 is Element of bool the carrier of x
y9 is Element of the carrier of x
x9 is Element of the carrier of x
y9 + x9 is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . (y9,x9) is Element of the carrier of x
[y9,x9] is set
{y9,x9} is non empty set
{y9} is non empty set
{{y9,x9},{y9}} is non empty set
the addF of x . [y9,x9] is set
q is set
x9 is (L,x)
the carrier of x9 is set
y9 is non empty (L,x)
the carrier of y9 is non empty set
p is Element of the carrier of x
x1 is Element of the carrier of x
x1 is Element of the carrier of y9
y1 is Element of the carrier of y9
x1 + y1 is Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the addF of y9 . (x1,y1) is Element of the carrier of y9
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the addF of y9 . [x1,y1] is set
the carrier of L is non empty set
y9 is Element of the carrier of L
x9 is Element of the carrier of x
y9 * x9 is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x . (y9,x9) is Element of the carrier of x
[y9,x9] is set
{y9,x9} is non empty set
{y9} is non empty set
{{y9,x9},{y9}} is non empty set
the lmult of x . [y9,x9] is set
p is set
x1 is (L,x)
the carrier of x1 is set
q is non empty (L,x)
the carrier of q is non empty set
x9 is Element of the carrier of q
y9 * x9 is Element of the carrier of q
the lmult of q is Relation-like [: the carrier of L, the carrier of q:] -defined the carrier of q -valued Function-like non empty total V18([: the carrier of L, the carrier of q:], the carrier of q) Element of bool [:[: the carrier of L, the carrier of q:], the carrier of q:]
[: the carrier of L, the carrier of q:] is Relation-like non empty set
[:[: the carrier of L, the carrier of q:], the carrier of q:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of q:], the carrier of q:] is non empty set
the lmult of q . (y9,x9) is Element of the carrier of q
[y9,x9] is set
{y9,x9} is non empty set
{{y9,x9},{y9}} is non empty set
the lmult of q . [y9,x9] is set
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y9 is Element of the carrier of x
x9 is Element of the carrier of x
y9 * x9 is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (y9,x9) is Element of the carrier of x
[y9,x9] is set
{y9,x9} is non empty set
{y9} is non empty set
{{y9,x9},{y9}} is non empty set
the multF of x . [y9,x9] is set
q is set
x9 is (L,x)
the carrier of x9 is set
y9 is non empty (L,x)
the carrier of y9 is non empty set
p is Element of the carrier of x
x1 is Element of the carrier of x
x1 is Element of the carrier of y9
y1 is Element of the carrier of y9
x1 * y1 is Element of the carrier of y9
the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the multF of y9 . (x1,y1) is Element of the carrier of y9
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the multF of y9 . [x1,y1] is set
y9 is set
x9 is (L,x)
the carrier of x9 is set
p is non empty (L,x)
1. p is Element of the carrier of p
the carrier of p is non empty set
the OneF of p is Element of the carrier of p
y9 is set
x9 is (L,x)
the carrier of x9 is set
p is non empty (L,x)
0. p is V54(p) Element of the carrier of p
the carrier of p is non empty set
the ZeroF of p is Element of the carrier of p
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
y is non empty Element of bool the carrier of x
bool (bool the carrier of x) is non empty set
y1 is Element of bool (bool the carrier of x)
y9 is set
x9 is (L,x)
the carrier of x9 is set
meet y1 is Element of bool the carrier of x
x9 is set
p is set
x1 is (L,x)
the carrier of x1 is set
x9 is (L) (L,x)
the carrier of x9 is set
p is non empty (L) (L,x)
the carrier of p is non empty set
bool the carrier of x is non empty Element of bool (bool the carrier of x)
x1 is (L,x)
the carrier of x1 is set
y1 is non empty (L) (L,x)
the carrier of y1 is non empty set
y9 is non empty (L) (L,x)
the carrier of y9 is non empty set
p is Element of the carrier of y9
x9 is Element of the carrier of y1
q is Element of the carrier of y9
the multF of y1 is Relation-like [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued Function-like non empty total V18([: the carrier of y1, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:]
[: the carrier of y1, the carrier of y1:] is Relation-like non empty set
[:[: the carrier of y1, the carrier of y1:], the carrier of y1:] is Relation-like non empty set
bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:] is non empty set
the multF of y1 . (x9,p) is set
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the multF of y1 . [x9,p] is set
x1 is Element of the carrier of y1
x9 * x1 is Element of the carrier of y1
the multF of y1 . (x9,x1) is Element of the carrier of y1
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the multF of y1 . [x9,x1] is set
x9 is Element of the carrier of x
y9 is Element of the carrier of x
x9 * y9 is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (x9,y9) is Element of the carrier of x
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
the multF of x . [x9,y9] is set
q * p is Element of the carrier of y9
the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the multF of y9 . (q,p) is Element of the carrier of y9
[q,p] is set
{q,p} is non empty set
{q} is non empty set
{{q,p},{q}} is non empty set
the multF of y9 . [q,p] is set
the multF of y9 . (x9,p) is set
the multF of y9 . [x9,p] is set
0. y1 is V54(y1) Element of the carrier of y1
the ZeroF of y1 is Element of the carrier of y1
0. x is V54(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
0. y9 is V54(y9) Element of the carrier of y9
the ZeroF of y9 is Element of the carrier of y9
the carrier of L is non empty set
p is Element of the carrier of y1
x1 is Element of the carrier of y9
the lmult of y1 is Relation-like [: the carrier of L, the carrier of y1:] -defined the carrier of y1 -valued Function-like non empty total V18([: the carrier of L, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:]
[: the carrier of L, the carrier of y1:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y1:], the carrier of y1:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y1:], the carrier of y1:] is non empty set
x9 is Element of the carrier of L
the lmult of y1 . (x9,p) is Element of the carrier of y1
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the lmult of y1 . [x9,p] is set
x9 * p is Element of the carrier of y1
q is Element of the carrier of x
x9 * q is Element of the carrier of x
the lmult of x is Relation-like [: the carrier of L, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of L, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of L, the carrier of x:], the carrier of x:]
[: the carrier of L, the carrier of x:] is Relation-like non empty set
[:[: the carrier of L, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of x:], the carrier of x:] is non empty set
the lmult of x . (x9,q) is Element of the carrier of x
[x9,q] is set
{x9,q} is non empty set
{{x9,q},{x9}} is non empty set
the lmult of x . [x9,q] is set
x9 * x1 is Element of the carrier of y9
the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]
[: the carrier of L, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set
the lmult of y9 . (x9,x1) is Element of the carrier of y9
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the lmult of y9 . [x9,x1] is set
the lmult of y9 . (x9,p) is set
the lmult of y9 . [x9,p] is set
1. y1 is Element of the carrier of y1
the OneF of y1 is Element of the carrier of y1
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
1. y9 is Element of the carrier of y9
the OneF of y9 is Element of the carrier of y9
p is Element of the carrier of y9
x9 is Element of the carrier of y1
q is Element of the carrier of y9
the addF of y1 is Relation-like [: the carrier of y1, the carrier of y1:] -defined the carrier of y1 -valued Function-like non empty total V18([: the carrier of y1, the carrier of y1:], the carrier of y1) Element of bool [:[: the carrier of y1, the carrier of y1:], the carrier of y1:]
the addF of y1 . (x9,p) is set
[x9,p] is set
{x9,p} is non empty set
{x9} is non empty set
{{x9,p},{x9}} is non empty set
the addF of y1 . [x9,p] is set
x1 is Element of the carrier of y1
x9 + x1 is Element of the carrier of y1
the addF of y1 . (x9,x1) is Element of the carrier of y1
[x9,x1] is set
{x9,x1} is non empty set
{{x9,x1},{x9}} is non empty set
the addF of y1 . [x9,x1] is set
x9 is Element of the carrier of x
y9 is Element of the carrier of x
x9 + y9 is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . (x9,y9) is Element of the carrier of x
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
the addF of x . [x9,y9] is set
q + p is Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
the addF of y9 . (q,p) is Element of the carrier of y9
[q,p] is set
{q,p} is non empty set
{q} is non empty set
{{q,p},{q}} is non empty set
the addF of y9 . [q,p] is set
the addF of y9 . (x9,p) is set
the addF of y9 . [x9,p] is set
L is non empty multMagma
x is non empty (L)
the carrier of x is non empty set
bool the carrier of x is non empty set
y is non empty Element of bool the carrier of x
(L,x,y) is non empty (L) (L,x)
the carrier of (L,x,y) is non empty set
y1 is (L) (L,x)
the carrier of y1 is set
L is non empty right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
bool the carrier of (L) is non empty set
Polynom-Ring L is non empty right_add-cancelable right_complementable strict add-associative right_zeroed doubleLoopStr
the carrier of (Polynom-Ring L) is non empty set
x is set
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x is non empty Element of bool the carrier of (L)
(L,(L),x) is non empty (L) (L,(L))
y1 is non empty Element of bool the carrier of (L)
x is non empty (L) (L)
(L,(L),y1) is non empty (L) (L,(L))
y9 is non empty Element of bool the carrier of (L)
y is non empty (L) (L)
(L,(L),y9) is non empty (L) (L,(L))
L is non empty right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
Polynom-Ring L is non empty right_add-cancelable right_complementable strict add-associative right_zeroed doubleLoopStr
the carrier of (Polynom-Ring L) is non empty set
x is Element of the carrier of (Polynom-Ring L)
y is Element of the carrier of (Polynom-Ring L)
y - x is Element of the carrier of (Polynom-Ring L)
- x is Element of the carrier of (Polynom-Ring L)
y + (- x) is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) is Relation-like [: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] -defined the carrier of (Polynom-Ring L) -valued Function-like non empty total V18([: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L)) associative Element of bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):]
[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] is Relation-like non empty set
[:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is Relation-like non empty set
bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is non empty set
the addF of (Polynom-Ring L) . (y,(- x)) is Element of the carrier of (Polynom-Ring L)
[y,(- x)] is set
{y,(- x)} is non empty set
{y} is non empty set
{{y,(- x)},{y}} is non empty set
the addF of (Polynom-Ring L) . [y,(- x)] is set
y1 is Element of the carrier of (Polynom-Ring L)
y1 + x is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (y1,x) is Element of the carrier of (Polynom-Ring L)
[y1,x] is set
{y1,x} is non empty set
{y1} is non empty set
{{y1,x},{y1}} is non empty set
the addF of (Polynom-Ring L) . [y1,x] is set
(- x) + x is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . ((- x),x) is Element of the carrier of (Polynom-Ring L)
[(- x),x] is set
{(- x),x} is non empty set
{(- x)} is non empty set
{{(- x),x},{(- x)}} is non empty set
the addF of (Polynom-Ring L) . [(- x),x] is set
y + ((- x) + x) is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (y,((- x) + x)) is Element of the carrier of (Polynom-Ring L)
[y,((- x) + x)] is set
{y,((- x) + x)} is non empty set
{{y,((- x) + x)},{y}} is non empty set
the addF of (Polynom-Ring L) . [y,((- x) + x)] is set
0. (Polynom-Ring L) is V54( Polynom-Ring L) Element of the carrier of (Polynom-Ring L)
the ZeroF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
y + (0. (Polynom-Ring L)) is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (y,(0. (Polynom-Ring L))) is Element of the carrier of (Polynom-Ring L)
[y,(0. (Polynom-Ring L))] is set
{y,(0. (Polynom-Ring L))} is non empty set
{{y,(0. (Polynom-Ring L))},{y}} is non empty set
the addF of (Polynom-Ring L) . [y,(0. (Polynom-Ring L))] is set
y is Element of the carrier of (Polynom-Ring L)
x is Element of the carrier of (Polynom-Ring L)
y + x is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) is Relation-like [: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] -defined the carrier of (Polynom-Ring L) -valued Function-like non empty total V18([: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L)) associative Element of bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):]
[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] is Relation-like non empty set
[:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is Relation-like non empty set
bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is non empty set
the addF of (Polynom-Ring L) . (y,x) is Element of the carrier of (Polynom-Ring L)
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the addF of (Polynom-Ring L) . [y,x] is set
y1 is Element of the carrier of (Polynom-Ring L)
y1 + x is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (y1,x) is Element of the carrier of (Polynom-Ring L)
[y1,x] is set
{y1,x} is non empty set
{y1} is non empty set
{{y1,x},{y1}} is non empty set
the addF of (Polynom-Ring L) . [y1,x] is set
x is Element of the carrier of (Polynom-Ring L)
y is Element of the carrier of (Polynom-Ring L)
y1 is Element of the carrier of (Polynom-Ring L)
y9 is Element of the carrier of (Polynom-Ring L)
y1 + y9 is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) is Relation-like [: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] -defined the carrier of (Polynom-Ring L) -valued Function-like non empty total V18([: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L)) associative Element of bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):]
[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] is Relation-like non empty set
[:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is Relation-like non empty set
bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is non empty set
the addF of (Polynom-Ring L) . (y1,y9) is Element of the carrier of (Polynom-Ring L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the addF of (Polynom-Ring L) . [y1,y9] is set
x9 is Element of the carrier of (Polynom-Ring L)
y1 + x9 is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (y1,x9) is Element of the carrier of (Polynom-Ring L)
[y1,x9] is set
{y1,x9} is non empty set
{{y1,x9},{y1}} is non empty set
the addF of (Polynom-Ring L) . [y1,x9] is set
L is non empty right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
bool the carrier of (L) is non empty set
Polynom-Ring L is non empty right_add-cancelable right_complementable strict Loop-like add-associative right_zeroed doubleLoopStr
the carrier of (Polynom-Ring L) is non empty set
y is non empty Element of bool the carrier of (L)
the carrier of L is non empty set
y1 is Element of the carrier of L
y9 is Element of the carrier of (L)
y1 * y9 is Element of the carrier of (L)
the lmult of (L) is Relation-like [: the carrier of L, the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of L, the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):]
[: the carrier of L, the carrier of (L):] is Relation-like non empty set
[:[: the carrier of L, the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of (L):], the carrier of (L):] is non empty set
the lmult of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the lmult of (L) . [y1,y9] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
p is Element of the carrier of L
p * x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
y1 is Element of the carrier of (L)
y9 is Element of the carrier of (L)
y1 + y9 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the addF of (L) . [y1,y9] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
1. (L) is Element of the carrier of (L)
the OneF of (L) is Element of the carrier of (L)
0. (L) is V54((L)) Element of the carrier of (L)
the ZeroF of (L) is Element of the carrier of (L)
y1 is Element of the carrier of (L)
y9 is Element of the carrier of (L)
y1 * y9 is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (y1,y9) is Element of the carrier of (L)
[y1,y9] is set
{y1,y9} is non empty set
{y1} is non empty set
{{y1,y9},{y1}} is non empty set
the multF of (L) . [y1,y9] is set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
x9 *' p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
1. (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
the OneF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
0. (Polynom-Ring L) is V54( Polynom-Ring L) Element of the carrier of (Polynom-Ring L)
the ZeroF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
L is non empty right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
(L) is non empty (L) (L)
the carrier of (L) is non empty set
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
the OneF of (L) is Element of the carrier of (L)
the ZeroF of (L) is Element of the carrier of (L)
doubleLoopStr(# the carrier of (L), the addF of (L), the multF of (L), the OneF of (L), the ZeroF of (L) #) is strict doubleLoopStr
Polynom-Ring L is non empty right_add-cancelable right_complementable strict Loop-like add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable add-associative right_zeroed (L) (L)
the carrier of (L) is non empty set
bool the carrier of (L) is non empty set
the carrier of (Polynom-Ring L) is non empty set
x is non empty Element of bool the carrier of (L)
(L,(L),x) is non empty (L) (L,(L))
x is non empty Element of bool the carrier of (L)
(L,(L),x) is non empty (L) (L,(L))
the addF of (Polynom-Ring L) is Relation-like [: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] -defined the carrier of (Polynom-Ring L) -valued Function-like non empty total V18([: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L)) associative Element of bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):]
[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] is Relation-like non empty set
[:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is Relation-like non empty set
bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):] is non empty set
x is Element of the carrier of (L)
y is Element of the carrier of (Polynom-Ring L)
the addF of (L) . (x,y) is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of (L) . [x,y] is set
the addF of (Polynom-Ring L) . (x,y) is set
the addF of (Polynom-Ring L) . [x,y] is set
y9 is non empty Element of bool the carrier of (L)
(L,(L),y9) is non empty (L) (L,(L))
y1 is Element of the carrier of (L)
x9 is non empty Element of bool the carrier of (L)
(L,(L),x9) is non empty (L) (L,(L))
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
q is non empty Element of bool the carrier of (L)
(L,(L),q) is non empty (L) (L,(L))
x + y1 is Element of the carrier of (L)
the addF of (L) . (x,y1) is Element of the carrier of (L)
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the addF of (L) . [x,y1] is set
x9 is Element of the carrier of (L)
y9 is Element of the carrier of (L)
x9 + y9 is Element of the carrier of (L)
the addF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) associative Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the addF of (L) . (x9,y9) is Element of the carrier of (L)
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
the addF of (L) . [x9,y9] is set
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
p + q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
x1 is Element of the carrier of (Polynom-Ring L)
x1 + y is Element of the carrier of (Polynom-Ring L)
the addF of (Polynom-Ring L) . (x1,y) is Element of the carrier of (Polynom-Ring L)
[x1,y] is set
{x1,y} is non empty set
{x1} is non empty set
{{x1,y},{x1}} is non empty set
the addF of (Polynom-Ring L) . [x1,y] is set
x9 is non empty Element of bool the carrier of (L)
(L,(L),x9) is non empty (L) (L,(L))
y is Element of the carrier of (Polynom-Ring L)
y9 is non empty Element of bool the carrier of (L)
(L,(L),y9) is non empty (L) (L,(L))
y1 is Element of the carrier of (L)
x9 is non empty Element of bool the carrier of (L)
(L,(L),x9) is non empty (L) (L,(L))
x is Element of the carrier of (L)
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set
q is non empty Element of bool the carrier of (L)
(L,(L),q) is non empty (L) (L,(L))
the multF of (L) . (x,y) is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of (L) . [x,y] is set
x * y1 is Element of the carrier of (L)
the multF of (L) . (x,y1) is Element of the carrier of (L)
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the multF of (L) . [x,y1] is set
x9 is Element of the carrier of (L)
y9 is Element of the carrier of (L)
x9 * y9 is Element of the carrier of (L)
the multF of (L) is Relation-like [: the carrier of (L), the carrier of (L):] -defined the carrier of (L) -valued Function-like non empty total V18([: the carrier of (L), the carrier of (L):], the carrier of (L)) Element of bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like non empty set
[:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is Relation-like non empty set
bool [:[: the carrier of (L), the carrier of (L):], the carrier of (L):] is non empty set
the multF of (L) . (x9,y9) is Element of the carrier of (L)
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
the multF of (L) . [x9,y9] is set
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
p *' q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
x1 is Element of the carrier of (Polynom-Ring L)
x1 * y is Element of the carrier of (Polynom-Ring L)
the multF of (Polynom-Ring L) is Relation-like [: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):] -defined the carrier of (Polynom-Ring L) -valued Function-like non empty total V18([: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L)) Element of bool [:[: the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L):], the carrier of (Polynom-Ring L):]
the multF of (Polynom-Ring L) . (x1,y) is Element of the carrier of (Polynom-Ring L)
[x1,y] is set
{x1,y} is non empty set
{x1} is non empty set
{{x1,y},{x1}} is non empty set
the multF of (Polynom-Ring L) . [x1,y] is set
the multF of (Polynom-Ring L) . (x,y) is set
the multF of (Polynom-Ring L) . [x,y] is set
x9 is non empty Element of bool the carrier of (L)
(L,(L),x9) is non empty (L) (L,(L))
1. (L) is Element of the carrier of (L)
1. (L) is Element of the carrier of (L)
the OneF of (L) is Element of the carrier of (L)
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
1. (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
the OneF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
x is non empty Element of bool the carrier of (L)
(L,(L),x) is non empty (L) (L,(L))
0. (L) is V54((L)) Element of the carrier of (L)
0. (L) is V54((L)) Element of the carrier of (L)
the ZeroF of (L) is Element of the carrier of (L)
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
0. (Polynom-Ring L) is V54( Polynom-Ring L) Element of the carrier of (Polynom-Ring L)
the ZeroF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)
x is non empty Element of bool the carrier of (L)
(L,(L),x) is non empty (L) (L,(L))
L is non empty right_add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed doubleLoopStr
(L) is non empty right_add-cancelable right_complementable unital right_unital well-unital left_unital add-associative right_zeroed (L) (L)
1_ (L) is Element of the carrier of (L)
the carrier of (L) is non empty set
1. (L) is Element of the carrier of (L)
the OneF of (L) is Element of the carrier of (L)
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]
the carrier of L is non empty set
[:NAT, the carrier of L:] is Relation-like non empty set
bool [:NAT, the carrier of L:] is non empty set