:: POLYALG1 semantic presentation

REAL is set

NAT is non empty V24() V25() V26() Element of bool REAL

bool REAL is non empty set

K425() is strict V192() doubleLoopStr

the carrier of K425() is set

NAT is non empty V24() V25() V26() set

bool NAT is non empty set

bool NAT is non empty set

COMPLEX is set

RAT is set

INT is set

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

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is non empty set

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

K285(1,NAT) is M15( NAT )

{} is Relation-like non-empty empty-yielding functional empty V24() V25() V26() V28() V29() V30() FinSequence-like FinSequence-membered V42() V43() ext-real non negative set

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

0 is Relation-like non-empty empty-yielding functional empty V24() V25() V26() V28() V29() V30() FinSequence-like FinSequence-membered V42() V43() ext-real non negative Element of NAT

len {} is V36() set

L is non empty doubleLoopStr

{0} is non empty set

the carrier of L is non empty set

[: the carrier of L,{0}:] is Relation-like non empty set

[:[: the carrier of L,{0}:],{0}:] is Relation-like non empty set

bool [:[: the carrier of L,{0}:],{0}:] is non empty set

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

[:[: the carrier of L,{0}:],NAT:] is Relation-like non empty set

bool [:[: the carrier of L,{0}:],NAT:] is non empty set

[:{0},{0}:] is Relation-like non empty set

[:[:{0},{0}:],{0}:] is Relation-like non empty set

bool [:[:{0},{0}:],{0}:] is non empty set

the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]

y is Element of {0}

x is Relation-like [: the carrier of L,{0}:] -defined {0} -valued Function-like non empty total V18([: the carrier of L,{0}:],{0}) Element of bool [:[: the carrier of L,{0}:],{0}:]

(L,{0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:], the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:],y,y,x) is (L) (L)

L is non empty doubleLoopStr

L is non empty doubleLoopStr

{0} is non empty set

the carrier of L is non empty set

[: the carrier of L,{0}:] is Relation-like non empty set

[:[: the carrier of L,{0}:],{0}:] is Relation-like non empty set

bool [:[: the carrier of L,{0}:],{0}:] is non empty set

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

[:[: the carrier of L,{0}:],NAT:] is Relation-like non empty set

bool [:[: the carrier of L,{0}:],NAT:] is non empty set

[:{0},{0}:] is Relation-like non empty set

[:[:{0},{0}:],{0}:] is Relation-like non empty set

bool [:[:{0},{0}:],{0}:] is non empty set

the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]

y is Element of {0}

x is Relation-like [: the carrier of L,{0}:] -defined {0} -valued Function-like non empty total V18([: the carrier of L,{0}:],{0}) Element of bool [:[: the carrier of L,{0}:],{0}:]

(L,{0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:], the Relation-like [:{0},{0}:] -defined {0} -valued Function-like non empty total V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:],y,y,x) is (L) (L)

y9 is non empty (L)

the carrier of y9 is non empty set

x9 is Element of the carrier of y9

p is Element of the carrier of y9

1. y9 is Element of the carrier of y9

the OneF of y9 is Element of the carrier of y9

x9 is Element of the carrier of y9

x9 * (1. y9) is Element of the carrier of y9

the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set

the multF of y9 . (x9,(1. y9)) is Element of the carrier of y9

[x9,(1. y9)] is set

{x9,(1. y9)} is non empty set

{x9} is non empty set

{{x9,(1. y9)},{x9}} is non empty set

the multF of y9 . [x9,(1. y9)] is set

p is Element of the carrier of y9

(1. y9) * p is Element of the carrier of y9

the multF of y9 . ((1. y9),p) is Element of the carrier of y9

[(1. y9),p] is set

{(1. y9),p} is non empty set

{(1. y9)} is non empty set

{{(1. y9),p},{(1. y9)}} is non empty set

the multF of y9 . [(1. y9),p] is set

x9 is Element of the carrier of y9

p is Element of the carrier of y9

x1 is Element of the carrier of y9

p + x1 is Element of the carrier of y9

the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set

the addF of y9 . (p,x1) is Element of the carrier of y9

[p,x1] is set

{p,x1} is non empty set

{p} is non empty set

{{p,x1},{p}} is non empty set

the addF of y9 . [p,x1] is set

x9 * (p + x1) is Element of the carrier of y9

the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

the multF of y9 . (x9,(p + x1)) is Element of the carrier of y9

[x9,(p + x1)] is set

{x9,(p + x1)} is non empty set

{x9} is non empty set

{{x9,(p + x1)},{x9}} is non empty set

the multF of y9 . [x9,(p + x1)] is set

x9 * p is Element of the carrier of y9

the multF of y9 . (x9,p) is Element of the carrier of y9

[x9,p] is set

{x9,p} is non empty set

{{x9,p},{x9}} is non empty set

the multF of y9 . [x9,p] is set

x9 * x1 is Element of the carrier of y9

the multF of y9 . (x9,x1) is Element of the carrier of y9

[x9,x1] is set

{x9,x1} is non empty set

{{x9,x1},{x9}} is non empty set

the multF of y9 . [x9,x1] is set

(x9 * p) + (x9 * x1) is Element of the carrier of y9

the addF of y9 . ((x9 * p),(x9 * x1)) is Element of the carrier of y9

[(x9 * p),(x9 * x1)] is set

{(x9 * p),(x9 * x1)} is non empty set

{(x9 * p)} is non empty set

{{(x9 * p),(x9 * x1)},{(x9 * p)}} is non empty set

the addF of y9 . [(x9 * p),(x9 * x1)] is set

(p + x1) * x9 is Element of the carrier of y9

the multF of y9 . ((p + x1),x9) is Element of the carrier of y9

[(p + x1),x9] is set

{(p + x1),x9} is non empty set

{(p + x1)} is non empty set

{{(p + x1),x9},{(p + x1)}} is non empty set

the multF of y9 . [(p + x1),x9] is set

p * x9 is Element of the carrier of y9

the multF of y9 . (p,x9) is Element of the carrier of y9

[p,x9] is set

{p,x9} is non empty set

{{p,x9},{p}} is non empty set

the multF of y9 . [p,x9] is set

x1 * x9 is Element of the carrier of y9

the multF of y9 . (x1,x9) is Element of the carrier of y9

[x1,x9] is set

{x1,x9} is non empty set

{x1} is non empty set

{{x1,x9},{x1}} is non empty set

the multF of y9 . [x1,x9] is set

(p * x9) + (x1 * x9) is Element of the carrier of y9

the addF of y9 . ((p * x9),(x1 * x9)) is Element of the carrier of y9

[(p * x9),(x1 * x9)] is set

{(p * x9),(x1 * x9)} is non empty set

{(p * x9)} is non empty set

{{(p * x9),(x1 * x9)},{(p * x9)}} is non empty set

the addF of y9 . [(p * x9),(x1 * x9)] is set

x9 is Element of the carrier of L

p is Element of the carrier of y9

x1 is Element of the carrier of y9

p + x1 is Element of the carrier of y9

the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set

the addF of y9 . (p,x1) is Element of the carrier of y9

[p,x1] is set

{p,x1} is non empty set

{p} is non empty set

{{p,x1},{p}} is non empty set

the addF of y9 . [p,x1] is set

x9 * (p + x1) is Element of the carrier of y9

the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]

[: the carrier of L, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set

the lmult of y9 . (x9,(p + x1)) is Element of the carrier of y9

[x9,(p + x1)] is set

{x9,(p + x1)} is non empty set

{x9} is non empty set

{{x9,(p + x1)},{x9}} is non empty set

the lmult of y9 . [x9,(p + x1)] is set

x9 * p is Element of the carrier of y9

the lmult of y9 . (x9,p) is Element of the carrier of y9

[x9,p] is set

{x9,p} is non empty set

{{x9,p},{x9}} is non empty set

the lmult of y9 . [x9,p] is set

x9 * x1 is Element of the carrier of y9

the lmult of y9 . (x9,x1) is Element of the carrier of y9

[x9,x1] is set

{x9,x1} is non empty set

{{x9,x1},{x9}} is non empty set

the lmult of y9 . [x9,x1] is set

(x9 * p) + (x9 * x1) is Element of the carrier of y9

the addF of y9 . ((x9 * p),(x9 * x1)) is Element of the carrier of y9

[(x9 * p),(x9 * x1)] is set

{(x9 * p),(x9 * x1)} is non empty set

{(x9 * p)} is non empty set

{{(x9 * p),(x9 * x1)},{(x9 * p)}} is non empty set

the addF of y9 . [(x9 * p),(x9 * x1)] is set

x9 is Element of the carrier of L

p is Element of the carrier of L

x9 + p is Element of the carrier of L

the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the addF of L . (x9,p) is Element of the carrier of L

[x9,p] is set

{x9,p} is non empty set

{x9} is non empty set

{{x9,p},{x9}} is non empty set

the addF of L . [x9,p] is set

x1 is Element of the carrier of y9

(x9 + p) * x1 is Element of the carrier of y9

the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]

[: the carrier of L, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set

the lmult of y9 . ((x9 + p),x1) is Element of the carrier of y9

[(x9 + p),x1] is set

{(x9 + p),x1} is non empty set

{(x9 + p)} is non empty set

{{(x9 + p),x1},{(x9 + p)}} is non empty set

the lmult of y9 . [(x9 + p),x1] is set

x9 * x1 is Element of the carrier of y9

the lmult of y9 . (x9,x1) is Element of the carrier of y9

[x9,x1] is set

{x9,x1} is non empty set

{{x9,x1},{x9}} is non empty set

the lmult of y9 . [x9,x1] is set

p * x1 is Element of the carrier of y9

the lmult of y9 . (p,x1) is Element of the carrier of y9

[p,x1] is set

{p,x1} is non empty set

{p} is non empty set

{{p,x1},{p}} is non empty set

the lmult of y9 . [p,x1] is set

(x9 * x1) + (p * x1) is Element of the carrier of y9

the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set

the addF of y9 . ((x9 * x1),(p * x1)) is Element of the carrier of y9

[(x9 * x1),(p * x1)] is set

{(x9 * x1),(p * x1)} is non empty set

{(x9 * x1)} is non empty set

{{(x9 * x1),(p * x1)},{(x9 * x1)}} is non empty set

the addF of y9 . [(x9 * x1),(p * x1)] is set

x9 is Element of the carrier of L

p is Element of the carrier of L

x9 * p is Element of the carrier of L

the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is Relation-like non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the multF of L . (x9,p) is Element of the carrier of L

[x9,p] is set

{x9,p} is non empty set

{x9} is non empty set

{{x9,p},{x9}} is non empty set

the multF of L . [x9,p] is set

x1 is Element of the carrier of y9

(x9 * p) * x1 is Element of the carrier of y9

the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]

[: the carrier of L, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set

the lmult of y9 . ((x9 * p),x1) is Element of the carrier of y9

[(x9 * p),x1] is set

{(x9 * p),x1} is non empty set

{(x9 * p)} is non empty set

{{(x9 * p),x1},{(x9 * p)}} is non empty set

the lmult of y9 . [(x9 * p),x1] is set

p * x1 is Element of the carrier of y9

the lmult of y9 . (p,x1) is Element of the carrier of y9

[p,x1] is set

{p,x1} is non empty set

{p} is non empty set

{{p,x1},{p}} is non empty set

the lmult of y9 . [p,x1] is set

x9 * (p * x1) is Element of the carrier of y9

the lmult of y9 . (x9,(p * x1)) is Element of the carrier of y9

[x9,(p * x1)] is set

{x9,(p * x1)} is non empty set

{{x9,(p * x1)},{x9}} is non empty set

the lmult of y9 . [x9,(p * x1)] is set

1. L is Element of the carrier of L

the OneF of L is Element of the carrier of L

x9 is Element of the carrier of y9

(1. L) * x9 is Element of the carrier of y9

the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]

[: the carrier of L, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set

the lmult of y9 . ((1. L),x9) is Element of the carrier of y9

[(1. L),x9] is set

{(1. L),x9} is non empty set

{(1. L)} is non empty set

{{(1. L),x9},{(1. L)}} is non empty set

the lmult of y9 . [(1. L),x9] is set

x9 is Element of the carrier of L

p is Element of the carrier of y9

x1 is Element of the carrier of y9

p * x1 is Element of the carrier of y9

the multF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set

the multF of y9 . (p,x1) is Element of the carrier of y9

[p,x1] is set

{p,x1} is non empty set

{p} is non empty set

{{p,x1},{p}} is non empty set

the multF of y9 . [p,x1] is set

x9 * (p * x1) is Element of the carrier of y9

the lmult of y9 is Relation-like [: the carrier of L, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of L, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:]

[: the carrier of L, the carrier of y9:] is Relation-like non empty set

[:[: the carrier of L, the carrier of y9:], the carrier of y9:] is Relation-like non empty set

bool [:[: the carrier of L, the carrier of y9:], the carrier of y9:] is non empty set

the lmult of y9 . (x9,(p * x1)) is Element of the carrier of y9

[x9,(p * x1)] is set

{x9,(p * x1)} is non empty set

{x9} is non empty set

{{x9,(p * x1)},{x9}} is non empty set

the lmult of y9 . [x9,(p * x1)] is set

x9 * p is Element of the carrier of y9

the lmult of y9 . (x9,p) is Element of the carrier of y9

[x9,p] is set

{x9,p} is non empty set

{{x9,p},{x9}} is non empty set

the lmult of y9 . [x9,p] is set

(x9 * p) * x1 is Element of the carrier of y9

the multF of y9 . ((x9 * p),x1) is Element of the carrier of y9

[(x9 * p),x1] is set

{(x9 * p),x1} is non empty set

{(x9 * p)} is non empty set

{{(x9 * p),x1},{(x9 * p)}} is non empty set

the multF of y9 . [(x9 * p),x1] is set

L is set

x is set

[:L,x:] is Relation-like set

[:[:L,x:],L:] is Relation-like set

bool [:[:L,x:],L:] is non empty set

y is Relation-like [:L,x:] -defined L -valued Function-like V18([:L,x:],L) Element of bool [:[:L,x:],L:]

dom y is Relation-like set

L is set

x is set

[:L,x:] is Relation-like set

[:[:L,x:],x:] is Relation-like set

bool [:[:L,x:],x:] is non empty set

y is Relation-like [:L,x:] -defined x -valued Function-like V18([:L,x:],x) Element of bool [:[:L,x:],x:]

dom y is Relation-like set

L is non empty doubleLoopStr

the carrier of L is non empty set

[:NAT, the carrier of L:] is Relation-like non empty set

bool [:NAT, the carrier of L:] is non empty set

0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]

1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of bool [:NAT, the carrier of L:]

{ b

x is non empty set

y1 is Element of x

y9 is Element of x

x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x9 + p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x1 is Element of x

[:x,x:] is Relation-like non empty set

[:[:x,x:],x:] is Relation-like non empty set

bool [:[:x,x:],x:] is non empty set

y1 is Relation-like [:x,x:] -defined x -valued Function-like non empty total V18([:x,x:],x) Element of bool [:[:x,x:],x:]

x9 is Element of x

p is Element of x

x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x1 *' q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x9 is Element of x

x9 is Relation-like [:x,x:] -defined x -valued Function-like non empty total V18([:x,x:],x) Element of bool [:[:x,x:],x:]

p is Element of the carrier of L

x1 is Element of x

q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

p * q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x9 is Element of x

[: the carrier of L,x:] is Relation-like non empty set

[:[: the carrier of L,x:],x:] is Relation-like non empty set

bool [:[: the carrier of L,x:],x:] is non empty set

p is Relation-like [: the carrier of L,x:] -defined x -valued Function-like non empty total V18([: the carrier of L,x:],x) Element of bool [:[: the carrier of L,x:],x:]

y is Element of x

y9 is Element of x

(L,x,y1,x9,y,y9,p) is (L) (L)

x1 is non empty (L) (L)

the carrier of x1 is non empty set

0. x1 is V54(x1) Element of the carrier of x1

the ZeroF of x1 is Element of the carrier of x1

1. x1 is Element of the carrier of x1

the OneF of x1 is Element of the carrier of x1

q is set

x9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

q is Element of the carrier of x1

x9 is Element of the carrier of x1

q + x9 is Element of the carrier of x1

the addF of x1 is Relation-like [: the carrier of x1, the carrier of x1:] -defined the carrier of x1 -valued Function-like non empty total V18([: the carrier of x1, the carrier of x1:], the carrier of x1) Element of bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:]

[: the carrier of x1, the carrier of x1:] is Relation-like non empty set

[:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is Relation-like non empty set

bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is non empty set

the addF of x1 . (q,x9) is Element of the carrier of x1

[q,x9] is set

{q,x9} is non empty set

{q} is non empty set

{{q,x9},{q}} is non empty set

the addF of x1 . [q,x9] is set

y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

y9 + x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

y1 . (q,x9) is set

y1 . [q,x9] is set

y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

c

y1 + c

q is Element of the carrier of x1

x9 is Element of the carrier of x1

q * x9 is Element of the carrier of x1

the multF of x1 is Relation-like [: the carrier of x1, the carrier of x1:] -defined the carrier of x1 -valued Function-like non empty total V18([: the carrier of x1, the carrier of x1:], the carrier of x1) Element of bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:]

[: the carrier of x1, the carrier of x1:] is Relation-like non empty set

[:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is Relation-like non empty set

bool [:[: the carrier of x1, the carrier of x1:], the carrier of x1:] is non empty set

the multF of x1 . (q,x9) is Element of the carrier of x1

[q,x9] is set

{q,x9} is non empty set

{q} is non empty set

{{q,x9},{q}} is non empty set

the multF of x1 . [q,x9] is set

y9 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

y9 *' x1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

x9 . (q,x9) is set

x9 . [q,x9] is set

y1 is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of bool [:NAT, the carrier of L:]

c

y1 *' c

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