:: BSPACE semantic presentation

REAL is set

NAT is non empty non trivial V23() V24() V25() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial V23() V24() V25() non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

COMPLEX is set

RAT is set

INT is set

{} is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() set

the functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() set is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() set

2 is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real positive V128() Element of NAT

1 is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real positive V128() Element of NAT

0 is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of NAT

K385(0,1,2) is non empty finite set

[:K385(0,1,2),K385(0,1,2):] is non empty finite set

[:[:K385(0,1,2),K385(0,1,2):],K385(0,1,2):] is non empty finite set

bool [:[:K385(0,1,2),K385(0,1,2):],K385(0,1,2):] is non empty finite V34() set

bool [:K385(0,1,2),K385(0,1,2):] is non empty finite V34() set

INT.Ring is doubleLoopStr

K587() is Relation-like [:INT,INT:] -defined INT -valued Function-like V18([:INT,INT:], INT ) Element of bool [:[:INT,INT:],INT:]

[:INT,INT:] is set

[:[:INT,INT:],INT:] is set

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

K589() is Relation-like [:INT,INT:] -defined INT -valued Function-like V18([:INT,INT:], INT ) Element of bool [:[:INT,INT:],INT:]

K444(1,INT) is V57() integer ext-real V128() Element of INT

K444(0,INT) is V57() integer ext-real V128() Element of INT

doubleLoopStr(# INT,K587(),K589(),K444(1,INT),K444(0,INT) #) is strict doubleLoopStr

the carrier of INT.Ring is set

[: the carrier of INT.Ring,NAT:] is set

bool [: the carrier of INT.Ring,NAT:] is non empty set

[:REAL,REAL:] is set

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

K532() is non empty strict multMagma

the carrier of K532() is non empty set

[:COMPLEX,COMPLEX:] is set

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

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

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

[:[:REAL,REAL:],REAL:] is set

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

[:RAT,RAT:] is set

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

[:[:RAT,RAT:],RAT:] is set

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

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

[:NAT,NAT:] is non empty non trivial non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

3 is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real positive V128() Element of NAT

bool {} is non empty finite V34() set

{{}} is non empty trivial finite V34() 1 -element set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

{ b

{1} is non empty trivial finite V34() 1 -element set

Seg 2 is non empty finite 2 -element Element of bool NAT

{ b

{1,2} is non empty finite V34() set

{{},1} is non empty finite V34() set

X is 1-sorted

[#] X is non proper Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty set

<*> ([#] X) is Relation-like NAT -defined [#] X -valued Function-like functional empty V23() V24() V25() V27() V28() V29() finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() integer ext-real V128() FinSequence of [#] X

X is 1-sorted

the carrier of X is set

f is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT

x1 is Relation-like NAT -defined the carrier of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X

dom x1 is finite Element of bool NAT

x1 . f is set

X is 1-sorted

the carrier of X is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom f is finite Element of bool NAT

x1 is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set

f . x1 is set

F

(F

the carrier of F

[#] F

bool the carrier of F

<*> ([#] F

<*> the carrier of F

INT.Ring 2 is doubleLoopStr

Segm 2 is Element of bool NAT

K533(2) is Relation-like [:(Segm 2),(Segm 2):] -defined Segm 2 -valued Function-like V18([:(Segm 2),(Segm 2):], Segm 2) Element of bool [:[:(Segm 2),(Segm 2):],(Segm 2):]

[:(Segm 2),(Segm 2):] is set

[:[:(Segm 2),(Segm 2):],(Segm 2):] is set

bool [:[:(Segm 2),(Segm 2):],(Segm 2):] is non empty set

K505(2) is Relation-like [:(Segm 2),(Segm 2):] -defined Segm 2 -valued Function-like V18([:(Segm 2),(Segm 2):], Segm 2) Element of bool [:[:(Segm 2),(Segm 2):],(Segm 2):]

K444(1,(Segm 2)) is Element of Segm 2

K444(0,(Segm 2)) is Element of Segm 2

doubleLoopStr(# (Segm 2),K533(2),K505(2),K444(1,(Segm 2)),K444(0,(Segm 2)) #) is strict doubleLoopStr

() is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V105() left_unital Abelian add-associative right_zeroed doubleLoopStr

[#] () is non empty non proper Element of bool the carrier of ()

the carrier of () is non empty non trivial set

bool the carrier of () is non empty set

X is Element of the carrier of ()

0. () is V50(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

1. () is V50(()) Element of the carrier of ()

the OneF of () is Element of the carrier of ()

(1. ()) + (1. ()) is Element of the carrier of ()

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

[: the carrier of (), the carrier of ():] is non empty set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set

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

the addF of () . ((1. ()),(1. ())) is Element of the carrier of ()

[(1. ()),(1. ())] is set

{(1. ()),(1. ())} is non empty finite set

{(1. ())} is non empty trivial finite 1 -element set

{{(1. ()),(1. ())},{(1. ())}} is non empty finite V34() set

the addF of () . [(1. ()),(1. ())] is set

1 + 1 is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT

(1 + 1) mod 2 is V57() integer ext-real V128() set

X is Element of the carrier of ()

f is Element of the carrier of ()

f is set

X is set

X is set

f is set

(X,f) is Element of the carrier of ()

x2 is set

x1 is set

(x1,x2) is Element of the carrier of ()

X is set

f is set

(X,f) is Element of the carrier of ()

x2 is set

x1 is set

(x1,x2) is Element of the carrier of ()

X is set

f is set

(X,f) is Element of the carrier of ()

x1 is set

x2 is set

(x1,x2) is Element of the carrier of ()

X is set

f is set

(X,f) is Element of the carrier of ()

x1 is set

(X,x1) is Element of the carrier of ()

X is set

x1 is set

(X,x1) is Element of the carrier of ()

f is set

(f,x1) is Element of the carrier of ()

X is set

({},X) is Element of the carrier of ()

X is set

bool X is non empty set

f is Element of bool X

x1 is Element of bool X

f \+\ x1 is Element of bool X

f \ x1 is set

x1 \ f is set

(f \ x1) \/ (x1 \ f) is set

x2 is Element of X

((f \+\ x1),x2) is Element of the carrier of ()

(f,x2) is Element of the carrier of ()

(x1,x2) is Element of the carrier of ()

(f,x2) + (x1,x2) is Element of the carrier of ()

the addF of () . ((f,x2),(x1,x2)) is Element of the carrier of ()

[(f,x2),(x1,x2)] is set

{(f,x2),(x1,x2)} is non empty finite set

{(f,x2)} is non empty trivial finite 1 -element set

{{(f,x2),(x1,x2)},{(f,x2)}} is non empty finite V34() set

the addF of () . [(f,x2),(x1,x2)] is set

X is set

f is set

x1 is set

(X,x1) is Element of the carrier of ()

(f,x1) is Element of the carrier of ()

x1 is set

(X,x1) is Element of the carrier of ()

(f,x1) is Element of the carrier of ()

x1 is set

(f,x1) is Element of the carrier of ()

(X,x1) is Element of the carrier of ()

X is set

bool X is non empty set

f is Element of the carrier of ()

x1 is Element of bool X

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

x2 is Element of bool X

X is set

bool X is non empty set

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

f is set

x1 is set

x2 is Element of bool X

y is Element of bool X

x2 \+\ y is Element of bool X

x2 \ y is set

y \ x2 is set

(x2 \ y) \/ (y \ x2) is set

f is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) Element of bool [:[:(bool X),(bool X):],(bool X):]

x1 is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) Element of bool [:[:(bool X),(bool X):],(bool X):]

x2 is Element of bool X

y is Element of bool X

x1 . (x2,y) is Element of bool X

[x2,y] is set

{x2,y} is non empty finite set

{x2} is non empty trivial finite 1 -element set

{{x2,y},{x2}} is non empty finite V34() set

x1 . [x2,y] is set

x2 \+\ y is Element of bool X

x2 \ y is set

y \ x2 is set

(x2 \ y) \/ (y \ x2) is set

x is Element of bool X

A is Element of bool X

x \+\ A is Element of bool X

x \ A is set

A \ x is set

(x \ A) \/ (A \ x) is set

x2 is Element of bool X

y is Element of bool X

x1 . (x2,y) is Element of bool X

[x2,y] is set

{x2,y} is non empty finite set

{x2} is non empty trivial finite 1 -element set

{{x2,y},{x2}} is non empty finite V34() set

x1 . [x2,y] is set

x2 \+\ y is Element of bool X

x2 \ y is set

y \ x2 is set

(x2 \ y) \/ (y \ x2) is set

f is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) Element of bool [:[:(bool X),(bool X):],(bool X):]

x1 is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) Element of bool [:[:(bool X),(bool X):],(bool X):]

dom f is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]

bool [:(bool X),(bool X):] is non empty set

x2 is set

f . x2 is set

x1 . x2 is set

y is set

x is set

[y,x] is set

{y,x} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,x},{y}} is non empty finite V34() set

l is Element of bool X

A is Element of bool X

f . (l,A) is Element of bool X

[l,A] is set

{l,A} is non empty finite set

{l} is non empty trivial finite 1 -element set

{{l,A},{l}} is non empty finite V34() set

f . [l,A] is set

l \+\ A is Element of bool X

l \ A is set

A \ l is set

(l \ A) \/ (A \ l) is set

x1 . (l,A) is Element of bool X

x1 . [l,A] is set

dom x1 is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]

X is set

bool X is non empty set

f is Element of the carrier of ()

x1 is Element of bool X

x2 is Element of bool X

x1 \+\ x2 is Element of bool X

x1 \ x2 is set

x2 \ x1 is set

(x1 \ x2) \/ (x2 \ x1) is set

(X,f,(x1 \+\ x2)) is Element of bool X

(X,f,x1) is Element of bool X

(X,f,x2) is Element of bool X

(X,f,x1) \+\ (X,f,x2) is Element of bool X

(X,f,x1) \ (X,f,x2) is set

(X,f,x2) \ (X,f,x1) is set

((X,f,x1) \ (X,f,x2)) \/ ((X,f,x2) \ (X,f,x1)) is set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

X is set

bool X is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f + x1 is Element of the carrier of ()

the addF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of () . [f,x1] is set

x2 is Element of bool X

(X,(f + x1),x2) is Element of bool X

(X,f,x2) is Element of bool X

(X,x1,x2) is Element of bool X

(X,f,x2) \+\ (X,x1,x2) is Element of bool X

(X,f,x2) \ (X,x1,x2) is set

(X,x1,x2) \ (X,f,x2) is set

((X,f,x2) \ (X,x1,x2)) \/ ((X,x1,x2) \ (X,f,x2)) is set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

x2 \+\ x2 is Element of bool X

x2 \ x2 is set

(x2 \ x2) \/ (x2 \ x2) is set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

X is set

bool X is non empty set

f is Element of bool X

(X,(1. ()),f) is Element of bool X

X is set

bool X is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f * x1 is Element of the carrier of ()

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

the multF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the multF of () . [f,x1] is set

x2 is Element of bool X

(X,x1,x2) is Element of bool X

(X,f,(X,x1,x2)) is Element of bool X

(X,(f * x1),x2) is Element of bool X

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

X is set

bool X is non empty set

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

f is set

x1 is set

y is Element of the carrier of ()

x2 is Element of bool X

(X,y,x2) is Element of bool X

f is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

x1 is Element of the carrier of ()

x2 is Element of bool X

f . (x1,x2) is Element of bool X

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

f . [x1,x2] is set

(X,x1,x2) is Element of bool X

y is Element of the carrier of ()

x is Element of bool X

(X,y,x) is Element of bool X

x1 is Element of the carrier of ()

x2 is Element of bool X

f . (x1,x2) is Element of bool X

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

f . [x1,x2] is set

(X,x1,x2) is Element of bool X

f is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

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

dom f is Relation-like the carrier of () -defined bool X -valued Element of bool [: the carrier of (),(bool X):]

bool [: the carrier of (),(bool X):] is non empty set

x2 is set

f . x2 is set

x1 . x2 is set

y is set

x is set

[y,x] is set

{y,x} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,x},{y}} is non empty finite V34() set

l is Element of the carrier of ()

A is Element of bool X

f . (l,A) is Element of bool X

[l,A] is set

{l,A} is non empty finite set

{l} is non empty trivial finite 1 -element set

{{l,A},{l}} is non empty finite V34() set

f . [l,A] is set

(X,l,A) is Element of bool X

x1 . (l,A) is Element of bool X

x1 . [l,A] is set

dom x1 is Relation-like the carrier of () -defined bool X -valued Element of bool [: the carrier of (),(bool X):]

X is set

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

x1 is Element of the carrier of (X)

x2 is Element of the carrier of (X)

x1 + x2 is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the addF of (X) . [x1,x2] is set

f + (x1 + x2) is Element of the carrier of (X)

the addF of (X) . (f,(x1 + x2)) is Element of the carrier of (X)

[f,(x1 + x2)] is set

{f,(x1 + x2)} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,(x1 + x2)},{f}} is non empty finite V34() set

the addF of (X) . [f,(x1 + x2)] is set

f + x1 is Element of the carrier of (X)

the addF of (X) . (f,x1) is Element of the carrier of (X)

[f,x1] is set

{f,x1} is non empty finite set

{{f,x1},{f}} is non empty finite V34() set

the addF of (X) . [f,x1] is set

(f + x1) + x2 is Element of the carrier of (X)

the addF of (X) . ((f + x1),x2) is Element of the carrier of (X)

[(f + x1),x2] is set

{(f + x1),x2} is non empty finite set

{(f + x1)} is non empty trivial finite 1 -element set

{{(f + x1),x2},{(f + x1)}} is non empty finite V34() set

the addF of (X) . [(f + x1),x2] is set

y is Element of bool X

x is Element of bool X

A is Element of bool X

x \+\ A is Element of bool X

x \ A is set

A \ x is set

(x \ A) \/ (A \ x) is set

y \+\ (x \+\ A) is Element of bool X

y \ (x \+\ A) is set

(x \+\ A) \ y is set

(y \ (x \+\ A)) \/ ((x \+\ A) \ y) is set

y \+\ x is Element of bool X

y \ x is set

x \ y is set

(y \ x) \/ (x \ y) is set

(y \+\ x) \+\ A is Element of bool X

(y \+\ x) \ A is set

A \ (y \+\ x) is set

((y \+\ x) \ A) \/ (A \ (y \+\ x)) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f + x1 is Element of the carrier of ()

the addF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of () . [f,x1] is set

f * x1 is Element of the carrier of ()

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

the multF of () . (f,x1) is Element of the carrier of ()

the multF of () . [f,x1] is set

x2 is Element of the carrier of (X)

y is Element of the carrier of (X)

f * x2 is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . (f,x2) is Element of the carrier of (X)

[f,x2] is set

{f,x2} is non empty finite set

{{f,x2},{f}} is non empty finite V34() set

the lmult of (X) . [f,x2] is set

x1 * y is Element of the carrier of (X)

the lmult of (X) . (x1,y) is Element of the carrier of (X)

[x1,y] is set

{x1,y} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,y},{x1}} is non empty finite V34() set

the lmult of (X) . [x1,y] is set

(f * x2) + (x1 * y) is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . ((f * x2),(x1 * y)) is Element of the carrier of (X)

[(f * x2),(x1 * y)] is set

{(f * x2),(x1 * y)} is non empty finite set

{(f * x2)} is non empty trivial finite 1 -element set

{{(f * x2),(x1 * y)},{(f * x2)}} is non empty finite V34() set

the addF of (X) . [(f * x2),(x1 * y)] is set

x2 + y is Element of the carrier of (X)

the addF of (X) . (x2,y) is Element of the carrier of (X)

[x2,y] is set

{x2,y} is non empty finite set

{x2} is non empty trivial finite 1 -element set

{{x2,y},{x2}} is non empty finite V34() set

the addF of (X) . [x2,y] is set

f * (x2 + y) is Element of the carrier of (X)

the lmult of (X) . (f,(x2 + y)) is Element of the carrier of (X)

[f,(x2 + y)] is set

{f,(x2 + y)} is non empty finite set

{{f,(x2 + y)},{f}} is non empty finite V34() set

the lmult of (X) . [f,(x2 + y)] is set

(f + x1) * x2 is Element of the carrier of (X)

the lmult of (X) . ((f + x1),x2) is Element of the carrier of (X)

[(f + x1),x2] is set

{(f + x1),x2} is non empty finite set

{(f + x1)} is non empty trivial finite 1 -element set

{{(f + x1),x2},{(f + x1)}} is non empty finite V34() set

the lmult of (X) . [(f + x1),x2] is set

(f * x1) * x2 is Element of the carrier of (X)

the lmult of (X) . ((f * x1),x2) is Element of the carrier of (X)

[(f * x1),x2] is set

{(f * x1),x2} is non empty finite set

{(f * x1)} is non empty trivial finite 1 -element set

{{(f * x1),x2},{(f * x1)}} is non empty finite V34() set

the lmult of (X) . [(f * x1),x2] is set

x1 * x2 is Element of the carrier of (X)

the lmult of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{{x1,x2},{x1}} is non empty finite V34() set

the lmult of (X) . [x1,x2] is set

f * (x1 * x2) is Element of the carrier of (X)

the lmult of (X) . (f,(x1 * x2)) is Element of the carrier of (X)

[f,(x1 * x2)] is set

{f,(x1 * x2)} is non empty finite set

{{f,(x1 * x2)},{f}} is non empty finite V34() set

the lmult of (X) . [f,(x1 * x2)] is set

x is Element of bool X

A is Element of bool X

(X,f,x) is Element of bool X

(X,x1,A) is Element of bool X

(X,f,x) \+\ (X,x1,A) is Element of bool X

(X,f,x) \ (X,x1,A) is set

(X,x1,A) \ (X,f,x) is set

((X,f,x) \ (X,x1,A)) \/ ((X,x1,A) \ (X,f,x)) is set

x \+\ A is Element of bool X

x \ A is set

A \ x is set

(x \ A) \/ (A \ x) is set

(X,f,(x \+\ A)) is Element of bool X

(X,(f + x1),x) is Element of bool X

(X,(f * x1),x) is Element of bool X

(X,x1,x) is Element of bool X

(X,f,(X,x1,x)) is Element of bool X

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

x1 is Element of the carrier of (X)

f + x1 is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (f,x1) is Element of the carrier of (X)

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of (X) . [f,x1] is set

x1 + f is Element of the carrier of (X)

the addF of (X) . (x1,f) is Element of the carrier of (X)

[x1,f] is set

{x1,f} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,f},{x1}} is non empty finite V34() set

the addF of (X) . [x1,f] is set

y is Element of bool X

x2 is Element of bool X

y \+\ x2 is Element of bool X

y \ x2 is set

x2 \ y is set

(y \ x2) \/ (x2 \ y) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

x1 is Element of the carrier of (X)

f + x1 is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (f,x1) is Element of the carrier of (X)

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of (X) . [f,x1] is set

x2 is Element of the carrier of (X)

(f + x1) + x2 is Element of the carrier of (X)

the addF of (X) . ((f + x1),x2) is Element of the carrier of (X)

[(f + x1),x2] is set

{(f + x1),x2} is non empty finite set

{(f + x1)} is non empty trivial finite 1 -element set

{{(f + x1),x2},{(f + x1)}} is non empty finite V34() set

the addF of (X) . [(f + x1),x2] is set

x1 + x2 is Element of the carrier of (X)

the addF of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the addF of (X) . [x1,x2] is set

f + (x1 + x2) is Element of the carrier of (X)

the addF of (X) . (f,(x1 + x2)) is Element of the carrier of (X)

[f,(x1 + x2)] is set

{f,(x1 + x2)} is non empty finite set

{{f,(x1 + x2)},{f}} is non empty finite V34() set

the addF of (X) . [f,(x1 + x2)] is set

y is Element of bool X

x is Element of bool X

A is Element of bool X

x \+\ A is Element of bool X

x \ A is set

A \ x is set

(x \ A) \/ (A \ x) is set

y \+\ (x \+\ A) is Element of bool X

y \ (x \+\ A) is set

(x \+\ A) \ y is set

(y \ (x \+\ A)) \/ ((x \+\ A) \ y) is set

y \+\ x is Element of bool X

y \ x is set

x \ y is set

(y \ x) \/ (x \ y) is set

(y \+\ x) \+\ A is Element of bool X

(y \+\ x) \ A is set

A \ (y \+\ x) is set

((y \+\ x) \ A) \/ (A \ (y \+\ x)) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

0. (X) is V50((X)) Element of the carrier of (X)

the ZeroF of (X) is Element of the carrier of (X)

f + (0. (X)) is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (f,(0. (X))) is Element of the carrier of (X)

[f,(0. (X))] is set

{f,(0. (X))} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,(0. (X))},{f}} is non empty finite V34() set

the addF of (X) . [f,(0. (X))] is set

x1 is Element of bool X

x2 is Element of bool X

x1 \+\ x2 is Element of bool X

x1 \ x2 is set

x2 \ x1 is set

(x1 \ x2) \/ (x2 \ x1) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

f + f is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (f,f) is Element of the carrier of (X)

[f,f] is set

{f,f} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,f},{f}} is non empty finite V34() set

the addF of (X) . [f,f] is set

0. (X) is V50((X)) Element of the carrier of (X)

the ZeroF of (X) is Element of the carrier of (X)

x1 is Element of bool X

x1 \+\ x1 is Element of bool X

x1 \ x1 is set

(x1 \ x1) \/ (x1 \ x1) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of (X)

x2 is Element of the carrier of (X)

x1 + x2 is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the addF of (X) . [x1,x2] is set

f * (x1 + x2) is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . (f,(x1 + x2)) is Element of the carrier of (X)

[f,(x1 + x2)] is set

{f,(x1 + x2)} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,(x1 + x2)},{f}} is non empty finite V34() set

the lmult of (X) . [f,(x1 + x2)] is set

f * x1 is Element of the carrier of (X)

the lmult of (X) . (f,x1) is Element of the carrier of (X)

[f,x1] is set

{f,x1} is non empty finite set

{{f,x1},{f}} is non empty finite V34() set

the lmult of (X) . [f,x1] is set

f * x2 is Element of the carrier of (X)

the lmult of (X) . (f,x2) is Element of the carrier of (X)

[f,x2] is set

{f,x2} is non empty finite set

{{f,x2},{f}} is non empty finite V34() set

the lmult of (X) . [f,x2] is set

(f * x1) + (f * x2) is Element of the carrier of (X)

the addF of (X) . ((f * x1),(f * x2)) is Element of the carrier of (X)

[(f * x1),(f * x2)] is set

{(f * x1),(f * x2)} is non empty finite set

{(f * x1)} is non empty trivial finite 1 -element set

{{(f * x1),(f * x2)},{(f * x1)}} is non empty finite V34() set

the addF of (X) . [(f * x1),(f * x2)] is set

y is Element of bool X

x is Element of bool X

y \+\ x is Element of bool X

y \ x is set

x \ y is set

(y \ x) \/ (x \ y) is set

(X,f,(y \+\ x)) is Element of bool X

(X,f,y) is Element of bool X

(X,f,x) is Element of bool X

(X,f,y) \+\ (X,f,x) is Element of bool X

(X,f,y) \ (X,f,x) is set

(X,f,x) \ (X,f,y) is set

((X,f,y) \ (X,f,x)) \/ ((X,f,x) \ (X,f,y)) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f + x1 is Element of the carrier of ()

the addF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of () . [f,x1] is set

x2 is Element of the carrier of (X)

(f + x1) * x2 is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . ((f + x1),x2) is Element of the carrier of (X)

[(f + x1),x2] is set

{(f + x1),x2} is non empty finite set

{(f + x1)} is non empty trivial finite 1 -element set

{{(f + x1),x2},{(f + x1)}} is non empty finite V34() set

the lmult of (X) . [(f + x1),x2] is set

f * x2 is Element of the carrier of (X)

the lmult of (X) . (f,x2) is Element of the carrier of (X)

[f,x2] is set

{f,x2} is non empty finite set

{{f,x2},{f}} is non empty finite V34() set

the lmult of (X) . [f,x2] is set

x1 * x2 is Element of the carrier of (X)

the lmult of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the lmult of (X) . [x1,x2] is set

(f * x2) + (x1 * x2) is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . ((f * x2),(x1 * x2)) is Element of the carrier of (X)

[(f * x2),(x1 * x2)] is set

{(f * x2),(x1 * x2)} is non empty finite set

{(f * x2)} is non empty trivial finite 1 -element set

{{(f * x2),(x1 * x2)},{(f * x2)}} is non empty finite V34() set

the addF of (X) . [(f * x2),(x1 * x2)] is set

y is Element of bool X

(X,(f + x1),y) is Element of bool X

(X,f,y) is Element of bool X

(X,x1,y) is Element of bool X

(X,f,y) \+\ (X,x1,y) is Element of bool X

(X,f,y) \ (X,x1,y) is set

(X,x1,y) \ (X,f,y) is set

((X,f,y) \ (X,x1,y)) \/ ((X,x1,y) \ (X,f,y)) is set

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f * x1 is Element of the carrier of ()

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

the multF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the multF of () . [f,x1] is set

x2 is Element of the carrier of (X)

(f * x1) * x2 is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . ((f * x1),x2) is Element of the carrier of (X)

[(f * x1),x2] is set

{(f * x1),x2} is non empty finite set

{(f * x1)} is non empty trivial finite 1 -element set

{{(f * x1),x2},{(f * x1)}} is non empty finite V34() set

the lmult of (X) . [(f * x1),x2] is set

x1 * x2 is Element of the carrier of (X)

the lmult of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the lmult of (X) . [x1,x2] is set

f * (x1 * x2) is Element of the carrier of (X)

the lmult of (X) . (f,(x1 * x2)) is Element of the carrier of (X)

[f,(x1 * x2)] is set

{f,(x1 * x2)} is non empty finite set

{{f,(x1 * x2)},{f}} is non empty finite V34() set

the lmult of (X) . [f,(x1 * x2)] is set

y is Element of bool X

(X,(f * x1),y) is Element of bool X

(X,x1,y) is Element of bool X

(X,f,(X,x1,y)) is Element of bool X

1_ () is Element of the carrier of ()

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of (X)

(1_ ()) * f is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . ((1_ ()),f) is Element of the carrier of (X)

[(1_ ()),f] is set

{(1_ ()),f} is non empty finite set

{(1_ ())} is non empty trivial finite 1 -element set

{{(1_ ()),f},{(1_ ())}} is non empty finite V34() set

the lmult of (X) . [(1_ ()),f] is set

x1 is Element of bool X

(X,(1_ ()),x1) is Element of bool X

X is set

(X) is non empty VectSpStr over ()

bool X is non empty set

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

[:(bool X),(bool X):] is non empty set

[:[:(bool X),(bool X):],(bool X):] is non empty set

bool [:[:(bool X),(bool X):],(bool X):] is non empty set

{} X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X

(X) is Relation-like [: the carrier of (),(bool X):] -defined bool X -valued Function-like V18([: the carrier of (),(bool X):], bool X) Element of bool [:[: the carrier of (),(bool X):],(bool X):]

[: the carrier of (),(bool X):] is non empty set

[:[: the carrier of (),(bool X):],(bool X):] is non empty set

bool [:[: the carrier of (),(bool X):],(bool X):] is non empty set

VectSpStr(# (bool X),(X),({} X),(X) #) is non empty strict VectSpStr over ()

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of (X)

x2 is Element of the carrier of (X)

x1 + x2 is Element of the carrier of (X)

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

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (X), the carrier of (X):], the carrier of (X):] is non empty set

the addF of (X) . (x1,x2) is Element of the carrier of (X)

[x1,x2] is set

{x1,x2} is non empty finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is non empty finite V34() set

the addF of (X) . [x1,x2] is set

f * (x1 + x2) is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):] is non empty set

the lmult of (X) . (f,(x1 + x2)) is Element of the carrier of (X)

[f,(x1 + x2)] is set

{f,(x1 + x2)} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,(x1 + x2)},{f}} is non empty finite V34() set

the lmult of (X) . [f,(x1 + x2)] is set

f * x1 is Element of the carrier of (X)

the lmult of (X) . (f,x1) is Element of the carrier of (X)

[f,x1] is set

{f,x1} is non empty finite set

{{f,x1},{f}} is non empty finite V34() set

the lmult of (X) . [f,x1] is set

f * x2 is Element of the carrier of (X)

the lmult of (X) . (f,x2) is Element of the carrier of (X)

[f,x2] is set

{f,x2} is non empty finite set

{{f,x2},{f}} is non empty finite V34() set

the lmult of (X) . [f,x2] is set

(f * x1) + (f * x2) is Element of the carrier of (X)

the addF of (X) . ((f * x1),(f * x2)) is Element of the carrier of (X)

[(f * x1),(f * x2)] is set

{(f * x1),(f * x2)} is non empty finite set

{(f * x1)} is non empty trivial finite 1 -element set

{{(f * x1),(f * x2)},{(f * x1)}} is non empty finite V34() set

the addF of (X) . [(f * x1),(f * x2)] is set

the carrier of (X) is non empty set

f is Element of the carrier of ()

x1 is Element of the carrier of ()

f + x1 is Element of the carrier of ()

the addF of () . (f,x1) is Element of the carrier of ()

[f,x1] is set

{f,x1} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,x1},{f}} is non empty finite V34() set

the addF of () . [f,x1] is set

x2 is Element of the carrier of (X)

(f + x1) * x2 is Element of the carrier of (X)

the lmult of (X) is Relation-like [: the carrier of (), the carrier of (X):] -defined the carrier of (X) -valued Function-like V18([: the carrier of (), the carrier of (X):], the carrier of (X)) Element of bool [:[: the carrier of (), the carrier of (X):], the carrier of (X):]

[: the carrier of (), the carrier of (X):] is non empty set

[:[: the carrier of (), the