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:]
{ b1 where b1 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:]
c14 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 + c14 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:]
c14 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 *' c14 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