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

RAT is set
INT is set
2 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative Element of NAT

bool 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 )

3 is non empty V24() V25() V26() V30() V42() V43() ext-real positive non negative Element of NAT

len {} is V36() set
L is non empty doubleLoopStr
is non empty set
the carrier of L is non empty set
[: the carrier of L,:] is Relation-like non empty set
[:[: the carrier of L,:],:] is Relation-like non empty set
bool [:[: the carrier of L,:],:] is non empty set
[: the carrier of L,:] --> 0 is Relation-like [: the carrier of L,:] -defined NAT -valued Function-like non empty total V18([: the carrier of L,:], NAT ) Element of bool [:[: the carrier of L,:],NAT:]
[:[: the carrier of L,:],NAT:] is Relation-like non empty set
bool [:[: the carrier of L,:],NAT:] is non empty set

bool is non empty set

y is Element of
x is Relation-like [: the carrier of L,:] -defined -valued Function-like non empty total V18([: the carrier of L,:],) Element of bool [:[: the carrier of L,:],:]
(L,, the Relation-like -defined -valued Function-like non empty total V18(,) Element of bool , the Relation-like -defined -valued Function-like non empty total V18(,) Element of bool ,y,y,x) is (L) (L)
L is non empty doubleLoopStr
L is non empty doubleLoopStr
is non empty set
the carrier of L is non empty set
[: the carrier of L,:] is Relation-like non empty set
[:[: the carrier of L,:],:] is Relation-like non empty set
bool [:[: the carrier of L,:],:] is non empty set
[: the carrier of L,:] --> 0 is Relation-like [: the carrier of L,:] -defined NAT -valued Function-like non empty total V18([: the carrier of L,:], NAT ) Element of bool [:[: the carrier of L,:],NAT:]
[:[: the carrier of L,:],NAT:] is Relation-like non empty set
bool [:[: the carrier of L,:],NAT:] is non empty set

bool is non empty set

y is Element of
x is Relation-like [: the carrier of L,:] -defined -valued Function-like non empty total V18([: the carrier of L,:],) Element of bool [:[: the carrier of L,:],:]
(L,, the Relation-like -defined -valued Function-like non empty total V18(,) Element of bool , the Relation-like -defined -valued Function-like non empty total V18(,) Element of bool ,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:]

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

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

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

L is non empty set

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 . 1 is set

dom x is non empty Element of bool NAT
x /. 1 is Element 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
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

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

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)*> ^ (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