:: 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₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V34() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁() is 1-sorted
(F₁()) is Relation-like NAT -defined the carrier of F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₁()
the carrier of F₁() is set
[#] F₁() is non proper Element of bool the carrier of F₁()
bool the carrier of F₁() is non empty set
<*> ([#] F₁()) is Relation-like NAT -defined [#] F₁() -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 [#] F₁()
<*> the carrier of F₁() is Relation-like NAT -defined the carrier of F₁() -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 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 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
f + x1 is Element of the carrier of ()
(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
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
f * x1 is Element of the carrier of ()
(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
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. ()),f},{(1. ())}} is non empty finite V34() set
the lmult of (X) . [(1. ()),f] 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 ()
X is set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
X is set
(X) is set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
(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
bool the carrier of (X) is non empty set
x1 is set
y is Element of bool X
x2 is Element of bool X
X is non empty set
(X) is Element of bool the carrier of (X)
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
the Element of X is Element of X
{ the Element of X} is non empty trivial finite 1 -element Element of bool X
X is non empty set
bool X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
(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 proper 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
(X) is non empty Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
f is Element of bool X
x1 is Element of bool X
X 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
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over X
the carrier of f is non empty set
the carrier of X is non empty non trivial set
x1 is Relation-like the carrier of f -defined the carrier of X -valued Function-like V18( the carrier of f, the carrier of X) Linear_Combination of f
x2 is Element of the carrier of f
x1 . x2 is set
x1 . x2 is Element of the carrier of X
[#] X is non empty non proper Element of bool the carrier of X
bool the carrier of X is non empty set
X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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 Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
len f is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
x1 is Element of X
x2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x2 is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
dom x2 is finite Element of bool NAT
y is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
x2 . y is set
f . y is set
((f . y),x1) is Element of the carrier of ()
rng x2 is finite set
y is set
x is set
x2 . x is set
f . x is set
((f . x),x1) is Element of the carrier of ()
y is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len y is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
x is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
y . x is set
f . x is set
((f . x),x1) is Element of the carrier of ()
x2 is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len x2 is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
y is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len y is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
x is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
x2 . x is set
y . x is set
f . x is set
((f . x),x1) is Element of the carrier of ()
(()) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*> ([#] ()) is Relation-like NAT -defined [#] () -valued Function-like functional empty proper 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 [#] ()
[:NAT,([#] ()):] is non empty non trivial non finite set
X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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 Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
the carrier of (X) is non empty set
[#] (X) is non empty non proper Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
<*> ([#] (X)) is Relation-like NAT -defined [#] (X) -valued Function-like functional empty proper 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)
[:NAT,([#] (X)):] is non empty non trivial non finite set
f is Element of X
(X,((X)),f) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len (X,((X)),f) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len ((X)) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
X is set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 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
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
((y \+\ x),x2) is Element of the carrier of ()
(y,x2) is Element of the carrier of ()
(x,x2) is Element of the carrier of ()
(y,x2) + (x,x2) is Element of the carrier of ()
the addF of () . ((y,x2),(x,x2)) is Element of the carrier of ()
[(y,x2),(x,x2)] is set
{(y,x2),(x,x2)} is non empty finite set
{(y,x2)} is non empty trivial finite 1 -element set
{{(y,x2),(x,x2)},{(y,x2)}} is non empty finite V34() set
the addF of () . [(y,x2),(x,x2)] is set
X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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 Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
x1 is Element of the carrier of (X)
<*x1*> is Relation-like NAT -defined the carrier of (X) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,x1] is set
{1,x1} is non empty finite set
{{1,x1},{1}} is non empty finite V34() set
{[1,x1]} is non empty trivial finite 1 -element set
f ^ <*x1*> is Relation-like NAT -defined the carrier of (X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
x2 is Element of X
(X,(f ^ <*x1*>),x2) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
(X,f,x2) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
(x1,x2) is Element of the carrier of ()
<*(x1,x2)*> is Relation-like NAT -defined the carrier of () -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
[1,(x1,x2)] is set
{1,(x1,x2)} is non empty finite set
{{1,(x1,x2)},{1}} is non empty finite V34() set
{[1,(x1,x2)]} is non empty trivial finite 1 -element set
(X,f,x2) ^ <*(x1,x2)*> is Relation-like NAT -defined the carrier of () -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len (X,(f ^ <*x1*>),x2) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len (f ^ <*x1*>) is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len f is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len <*x1*> is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len f) + (len <*x1*>) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len f) + 1 is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
A is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
(X,(f ^ <*x1*>),x2) . A is set
((X,f,x2) ^ <*(x1,x2)*>) . A is set
dom (X,f,x2) is finite Element of bool NAT
len (X,f,x2) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
Seg (len (X,f,x2)) is finite len (X,f,x2) -element Element of bool NAT
{ b₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= len (X,f,x2) ) } is set
Seg (len f) is finite len f -element Element of bool NAT
{ b₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
(X,f,x2) . A is set
f . A is set
((f . A),x2) is Element of the carrier of ()
dom f is finite Element of bool NAT
(f ^ <*x1*>) . A is set
(((f ^ <*x1*>) . A),x2) is Element of the carrier of ()
dom <*(x1,x2)*> is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V34() 1 -element Element of bool NAT
len (X,f,x2) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
<*(x1,x2)*> . 1 is set
dom <*x1*> is non empty trivial finite 1 -element Element of bool NAT
(f ^ <*x1*>) . A is set
<*x1*> . 1 is set
len ((X,f,x2) ^ <*(x1,x2)*>) is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len (X,f,x2) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len <*(x1,x2)*> is non empty V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len (X,f,x2)) + (len <*(x1,x2)*>) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len f) + (len <*(x1,x2)*>) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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 Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
Sum f is Element of the carrier of (X)
x1 is Element of X
((Sum f),x1) is Element of the carrier of ()
(X,f,x1) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum (X,f,x1) is Element of the carrier of ()
((X)) is Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[#] (X) is non empty non proper Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
<*> ([#] (X)) is Relation-like NAT -defined [#] (X) -valued Function-like functional empty proper 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)
[:NAT,([#] (X)):] is non empty non trivial non finite set
Sum ((X)) is Element of the carrier of (X)
((Sum ((X))),x1) is Element of the carrier of ()
(X,((X)),x1) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum (X,((X)),x1) is Element of the carrier of ()
0. (X) is V50((X)) Element of the carrier of (X)
the ZeroF of (X) is Element of the carrier of (X)
y is Element of bool X
(y,x1) is Element of the carrier of ()
y is Relation-like NAT -defined the carrier of (X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
Sum y is Element of the carrier of (X)
((Sum y),x1) is Element of the carrier of ()
(X,y,x1) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum (X,y,x1) is Element of the carrier of ()
x is Element of the carrier of (X)
<*x*> is Relation-like NAT -defined the carrier of (X) -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V34() set
{[1,x]} is non empty trivial finite 1 -element set
y ^ <*x*> is Relation-like NAT -defined the carrier of (X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
Sum (y ^ <*x*>) is Element of the carrier of (X)
((Sum (y ^ <*x*>)),x1) is Element of the carrier of ()
(X,(y ^ <*x*>),x1) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum (X,(y ^ <*x*>),x1) is Element of the carrier of ()
Sum <*x*> is Element of the carrier of (X)
(Sum y) + (Sum <*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) . ((Sum y),(Sum <*x*>)) is Element of the carrier of (X)
[(Sum y),(Sum <*x*>)] is set
{(Sum y),(Sum <*x*>)} is non empty finite set
{(Sum y)} is non empty trivial finite 1 -element set
{{(Sum y),(Sum <*x*>)},{(Sum y)}} is non empty finite V34() set
the addF of (X) . [(Sum y),(Sum <*x*>)] is set
(((Sum y) + (Sum <*x*>)),x1) is Element of the carrier of ()
(Sum y) + x is Element of the carrier of (X)
the addF of (X) . ((Sum y),x) is Element of the carrier of (X)
[(Sum y),x] is set
{(Sum y),x} is non empty finite set
{{(Sum y),x},{(Sum y)}} is non empty finite V34() set
the addF of (X) . [(Sum y),x] is set
(((Sum y) + x),x1) is Element of the carrier of ()
(x,x1) is Element of the carrier of ()
((Sum y),x1) + (x,x1) is Element of the carrier of ()
the addF of () . (((Sum y),x1),(x,x1)) is Element of the carrier of ()
[((Sum y),x1),(x,x1)] is set
{((Sum y),x1),(x,x1)} is non empty finite set
{((Sum y),x1)} is non empty trivial finite 1 -element set
{{((Sum y),x1),(x,x1)},{((Sum y),x1)}} is non empty finite V34() set
the addF of () . [((Sum y),x1),(x,x1)] is set
<*(x,x1)*> is Relation-like NAT -defined the carrier of () -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
[1,(x,x1)] is set
{1,(x,x1)} is non empty finite set
{{1,(x,x1)},{1}} is non empty finite V34() set
{[1,(x,x1)]} is non empty trivial finite 1 -element set
Sum <*(x,x1)*> is Element of the carrier of ()
(Sum (X,y,x1)) + (Sum <*(x,x1)*>) is Element of the carrier of ()
the addF of () . ((Sum (X,y,x1)),(Sum <*(x,x1)*>)) is Element of the carrier of ()
[(Sum (X,y,x1)),(Sum <*(x,x1)*>)] is set
{(Sum (X,y,x1)),(Sum <*(x,x1)*>)} is non empty finite set
{(Sum (X,y,x1))} is non empty trivial finite 1 -element set
{{(Sum (X,y,x1)),(Sum <*(x,x1)*>)},{(Sum (X,y,x1))}} is non empty finite V34() set
the addF of () . [(Sum (X,y,x1)),(Sum <*(x,x1)*>)] is set
(X,y,x1) ^ <*(x,x1)*> is Relation-like NAT -defined the carrier of () -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum ((X,y,x1) ^ <*(x,x1)*>) is Element of the carrier of ()
X is non empty set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 proper 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 Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Carrier f is finite Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
x1 is Element of the carrier of (X)
((),(X),f,x1) is Element of the carrier of ()
X is functional empty V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() set
(X) is Element of bool the carrier of (X)
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool X is non empty finite V34() set
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() set
{} X is functional empty non proper 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
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
f is set
x1 is functional empty non proper V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool X
X is set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 ()
(X) is Element of bool the carrier of (X)
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
f is non empty set
(f) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool f is non empty set
(f) is Relation-like [:(bool f),(bool f):] -defined bool f -valued Function-like V18([:(bool f),(bool f):], bool f) Element of bool [:[:(bool f),(bool f):],(bool f):]
[:(bool f),(bool f):] is non empty set
[:[:(bool f),(bool f):],(bool f):] is non empty set
bool [:[:(bool f),(bool f):],(bool f):] is non empty set
{} f is functional empty proper V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool f
(f) is Relation-like [: the carrier of (),(bool f):] -defined bool f -valued Function-like V18([: the carrier of (),(bool f):], bool f) Element of bool [:[: the carrier of (),(bool f):],(bool f):]
[: the carrier of (),(bool f):] is non empty set
[:[: the carrier of (),(bool f):],(bool f):] is non empty set
bool [:[: the carrier of (),(bool f):],(bool f):] is non empty set
VectSpStr(# (bool f),(f),({} f),(f) #) is non empty strict VectSpStr over ()
(f) is non empty Element of bool the carrier of (f)
the carrier of (f) is non empty set
bool the carrier of (f) is non empty set
{ b₁ where b₁ is Element of bool f : b₁ is 1 -element } is set
0. (f) is V50((f)) Element of the carrier of (f)
the ZeroF of (f) is Element of the carrier of (f)
y is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of (f)
Sum y is Element of the carrier of (f)
Carrier y is finite Element of bool the carrier of (f)
y ! (Carrier y) is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of Carrier y
l is Element of the carrier of (f)
z is Element of bool f
f is Element of the carrier of (f)
{f} is non empty trivial finite 1 -element Element of bool the carrier of (f)
y ! {f} is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of {f}
(Carrier y) \ {f} is finite Element of bool the carrier of (f)
y ! ((Carrier y) \ {f}) is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of (Carrier y) \ {f}
m is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of (Carrier y) \ {f}
Sum m is Element of the carrier of (f)
g is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of {f}
Sum g is Element of the carrier of (f)
((),(f),g,f) is Element of the carrier of ()
((),(f),g,f) * f is Element of the carrier of (f)
the lmult of (f) is Relation-like [: the carrier of (), the carrier of (f):] -defined the carrier of (f) -valued Function-like V18([: the carrier of (), the carrier of (f):], the carrier of (f)) Element of bool [:[: the carrier of (), the carrier of (f):], the carrier of (f):]
[: the carrier of (), the carrier of (f):] is non empty set
[:[: the carrier of (), the carrier of (f):], the carrier of (f):] is non empty set
bool [:[: the carrier of (), the carrier of (f):], the carrier of (f):] is non empty set
the lmult of (f) . (((),(f),g,f),f) is Element of the carrier of (f)
[((),(f),g,f),f] is set
{((),(f),g,f),f} is non empty finite set
{((),(f),g,f)} is non empty trivial finite 1 -element set
{{((),(f),g,f),f},{((),(f),g,f)}} is non empty finite V34() set
the lmult of (f) . [((),(f),g,f),f] is set
m is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of Carrier y
((),(f),m,f) is Element of the carrier of ()
c₁₅ is Element of bool f
x is Element of f
{x} is non empty trivial finite 1 -element Element of bool f
(z,x) is Element of the carrier of ()
F is Element of bool f
(F,x) is Element of the carrier of ()
F is Element of f
{F} is non empty trivial finite 1 -element Element of bool f
n is Element of bool f
(n,x) is Element of the carrier of ()
Carrier m is finite Element of bool the carrier of (f)
F is Relation-like NAT -defined the carrier of (f) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)
rng F is finite set
m (#) F is Relation-like NAT -defined the carrier of (f) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)
Sum (m (#) F) is Element of the carrier of (f)
((Sum (m (#) F)),x) is Element of the carrier of ()
(f,(m (#) F),x) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum (f,(m (#) F),x) is Element of the carrier of ()
F is Relation-like NAT -defined the carrier of (f) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)
rng F is finite set
m (#) F is Relation-like NAT -defined the carrier of (f) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)
(f,(m (#) F),x) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len F is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len F) |-> (0. ()) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of (len F) -tuples_on the carrier of ()
(len F) -tuples_on the carrier of () is FinSequenceSet of the carrier of ()
the carrier of () * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ()
{ b₁ where b₁ is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () * : len b₁ = len F } is set
Seg (len F) is finite len F -element Element of bool NAT
{ b₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
K90((Seg (len F)),(0. ())) is Relation-like Seg (len F) -defined {(0. ())} -valued Function-like V18( Seg (len F),{(0. ())}) finite Element of bool [:(Seg (len F)),{(0. ())}:]
{(0. ())} is non empty trivial finite 1 -element set
[:(Seg (len F)),{(0. ())}:] is finite set
bool [:(Seg (len F)),{(0. ())}:] is non empty finite V34() set
len (m (#) F) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len (f,(m (#) F),x) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
k is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
(f,(m (#) F),x) . k is set
((len F) |-> (0. ())) . k is set
dom (m (#) F) is finite Element of bool NAT
(m (#) F) . k is set
F /. k is Element of the carrier of (f)
((),(f),m,(F /. k)) is Element of the carrier of ()
((),(f),m,(F /. k)) * (F /. k) is Element of the carrier of (f)
the lmult of (f) . (((),(f),m,(F /. k)),(F /. k)) is Element of the carrier of (f)
[((),(f),m,(F /. k)),(F /. k)] is set
{((),(f),m,(F /. k)),(F /. k)} is non empty finite set
{((),(f),m,(F /. k))} is non empty trivial finite 1 -element set
{{((),(f),m,(F /. k)),(F /. k)},{((),(f),m,(F /. k))}} is non empty finite V34() set
the lmult of (f) . [((),(f),m,(F /. k)),(F /. k)] is set
{z} is non empty trivial finite 1 -element Element of bool (bool f)
bool (bool f) is non empty set
(Carrier y) \ {z} is finite Element of bool the carrier of (f)
dom F is finite Element of bool NAT
F . k is set
Fk is Element of bool f
(((m (#) F) . k),x) is Element of the carrier of ()
dom ((len F) |-> (0. ())) is finite Element of bool NAT
len ((len F) |-> (0. ())) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
len F is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT
(len F) |-> (0. ()) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of (len F) -tuples_on the carrier of ()
(len F) -tuples_on the carrier of () is FinSequenceSet of the carrier of ()
the carrier of () * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ()
{ b₁ where b₁ is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () * : len b₁ = len F } is set
Seg (len F) is finite len F -element Element of bool NAT
{ b₁ where b₁ is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
K90((Seg (len F)),(0. ())) is Relation-like Seg (len F) -defined {(0. ())} -valued Function-like V18( Seg (len F),{(0. ())}) finite Element of bool [:(Seg (len F)),{(0. ())}:]
{(0. ())} is non empty trivial finite 1 -element set
[:(Seg (len F)),{(0. ())}:] is finite set
bool [:(Seg (len F)),{(0. ())}:] is non empty finite V34() set
g + m is Relation-like the carrier of (f) -defined the carrier of () -valued Function-like V18( the carrier of (f), the carrier of ()) Linear_Combination of (f)
Sum m is Element of the carrier of (f)
(Sum m) + (Sum g) is Element of the carrier of (f)
the addF of (f) is Relation-like [: the carrier of (f), the carrier of (f):] -defined the carrier of (f) -valued Function-like V18([: the carrier of (f), the carrier of (f):], the carrier of (f)) Element of bool [:[: the carrier of (f), the carrier of (f):], the carrier of (f):]
[: the carrier of (f), the carrier of (f):] is non empty set
[:[: the carrier of (f), the carrier of (f):], the carrier of (f):] is non empty set
bool [:[: the carrier of (f), the carrier of (f):], the carrier of (f):] is non empty set
the addF of (f) . ((Sum m),(Sum g)) is Element of the carrier of (f)
[(Sum m),(Sum g)] is set
{(Sum m),(Sum g)} is non empty finite set
{(Sum m)} is non empty trivial finite 1 -element set
{{(Sum m),(Sum g)},{(Sum m)}} is non empty finite V34() set
the addF of (f) . [(Sum m),(Sum g)] is set
x is Element of bool f
n \+\ c₁₅ is Element of bool f
n \ c₁₅ is set
c₁₅ \ n is set
(n \ c₁₅) \/ (c₁₅ \ n) is set
(x,x) is Element of the carrier of ()
(c₁₅,x) is Element of the carrier of ()
(n,x) + (c₁₅,x) is Element of the carrier of ()
the addF of () . ((n,x),(c₁₅,x)) is Element of the carrier of ()
[(n,x),(c₁₅,x)] is set
{(n,x),(c₁₅,x)} is non empty finite set
{(n,x)} is non empty trivial finite 1 -element set
{{(n,x),(c₁₅,x)},{(n,x)}} is non empty finite V34() set
the addF of () . [(n,x),(c₁₅,x)] is set
X is set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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
x1 is set
f is Element of the carrier of (X)
{x1} is non empty trivial finite 1 -element set
(X) is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
X is finite set
bool X is non empty finite V34() set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() 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
(X) is Element of bool the carrier of (X)
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
f is finite Element of bool X
ZeroLC (X) is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
y is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum y 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)
y is set
x is set
{y} is non empty trivial finite 1 -element set
x \/ {y} is non empty set
A is finite Element of bool X
l is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum l is Element of the carrier of (X)
l is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum l is Element of the carrier of (X)
{} (X) is functional empty proper V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer linearly-independent ext-real V128() Element of bool the carrier of (X)
ZeroLC (X) is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
f is Element of the carrier of (X)
z is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of {} (X)
z +* (f,(1_ ())) is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Element of bool [: the carrier of (X), the carrier of ():]
[: the carrier of (X), the carrier of ():] is non empty set
bool [: the carrier of (X), the carrier of ():] is non empty set
{f} is non empty trivial finite 1 -element Element of bool the carrier of (X)
({} (X)) \/ {f} is non empty finite Element of bool the carrier of (X)
dom z is Element of bool the carrier of (X)
[#] (X) is non empty non proper Element of bool the carrier of (X)
m is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of {f}
((),(X),m,f) is Element of the carrier of ()
l + m is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
n is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum n is Element of the carrier of (X)
Sum m is Element of the carrier of (X)
(Sum l) + (Sum m) 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) . ((Sum l),(Sum m)) is Element of the carrier of (X)
[(Sum l),(Sum m)] is set
{(Sum l),(Sum m)} is non empty finite set
{(Sum l)} is non empty trivial finite 1 -element set
{{(Sum l),(Sum m)},{(Sum l)}} is non empty finite V34() set
the addF of (X) . [(Sum l),(Sum m)] is set
((),(X),m,f) * 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) . (((),(X),m,f),f) is Element of the carrier of (X)
[((),(X),m,f),f] is set
{((),(X),m,f),f} is non empty finite set
{((),(X),m,f)} is non empty trivial finite 1 -element set
{{((),(X),m,f),f},{((),(X),m,f)}} is non empty finite V34() set
the lmult of (X) . [((),(X),m,f),f] is set
(Sum l) + (((),(X),m,f) * f) is Element of the carrier of (X)
the addF of (X) . ((Sum l),(((),(X),m,f) * f)) is Element of the carrier of (X)
[(Sum l),(((),(X),m,f) * f)] is set
{(Sum l),(((),(X),m,f) * f)} is non empty finite set
{{(Sum l),(((),(X),m,f) * f)},{(Sum l)}} is non empty finite V34() set
the addF of (X) . [(Sum l),(((),(X),m,f) * f)] is set
(Sum l) + f is Element of the carrier of (X)
the addF of (X) . ((Sum l),f) is Element of the carrier of (X)
[(Sum l),f] is set
{(Sum l),f} is non empty finite set
{{(Sum l),f},{(Sum l)}} is non empty finite V34() set
the addF of (X) . [(Sum l),f] is set
g is finite Element of bool X
A \+\ g is finite Element of bool X
A \ g is finite set
g \ A is finite set
(A \ g) \/ (g \ A) is finite set
A \/ {y} is non empty finite set
A /\ {y} is finite Element of bool X
(A \/ {y}) \ (A /\ {y}) is finite Element of bool (A \/ {y})
bool (A \/ {y}) is non empty finite V34() set
(A \/ {y}) \ {} is finite Element of bool (A \/ {y})
y is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum y is Element of the carrier of (X)
X is finite set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool X is non empty finite V34() set
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() 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 Element of bool the carrier of (X)
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
Lin (X) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed M8((),(X))
x2 is Element of the carrier of (X)
y is finite Element of bool X
x is set
A is finite Element of bool X
l is Relation-like the carrier of (X) -defined the carrier of () -valued Function-like V18( the carrier of (X), the carrier of ()) Linear_Combination of (X)
Sum l is Element of the carrier of (X)
X is finite set
(X) is Element of bool the carrier of (X)
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool X is non empty finite V34() set
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() 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
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
Lin (X) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed M8((),(X))
X is finite set
(X) is Element of bool the carrier of (X)
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool X is non empty finite V34() set
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() 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
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
X is finite set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over ()
bool X is non empty finite V34() set
(X) is Relation-like [:(bool X),(bool X):] -defined bool X -valued Function-like V18([:(bool X),(bool X):], bool X) finite Element of bool [:[:(bool X),(bool X):],(bool X):]
[:(bool X),(bool X):] is non empty finite set
[:[:(bool X),(bool X):],(bool X):] is non empty finite set
bool [:[:(bool X),(bool X):],(bool X):] is non empty finite V34() 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 finite Element of bool the carrier of (X)
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
X is set
(X) is Element of bool the carrier of (X)
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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
bool the carrier of (X) is non empty set
{ b₁ where b₁ is Element of bool X : b₁ is 1 -element } is set
card (X) is V23() V24() V25() cardinal set
card X is V23() V24() V25() cardinal set
f is set
{f} is non empty trivial finite 1 -element set
f is Relation-like Function-like set
dom f is set
rng f is set
x1 is set
x2 is set
f . x2 is set
{x2} is non empty trivial finite 1 -element set
y is Element of bool X
x1 is set
x2 is non empty set
bool x2 is non empty set
x is Element of bool x2
y is non empty trivial finite 1 -element Element of bool x2
x is Element of x2
{x} is non empty trivial finite 1 -element Element of bool x2
f . x is set
x1 is set
x2 is set
f . x1 is set
f . x2 is set
{x1} is non empty trivial finite 1 -element set
{x2} is non empty trivial finite 1 -element set
X is set
(X) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed 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 ()
[#] (X) is non empty non proper Element of bool the carrier of (X)
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
card ([#] (X)) is non empty V23() V24() V25() cardinal set
card X is V23() V24() V25() cardinal set
exp (2,(card X)) is V23() V24() V25() cardinal set
({}) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional VectSpStr over ()
({}) is Relation-like [:(bool {}),(bool {}):] -defined bool {} -valued Function-like V18([:(bool {}),(bool {}):], bool {}) finite Element of bool [:[:(bool {}),(bool {}):],(bool {}):]
[:(bool {}),(bool {}):] is non empty finite set
[:[:(bool {}),(bool {}):],(bool {}):] is non empty finite set
bool [:[:(bool {}),(bool {}):],(bool {}):] is non empty finite V34() set
{} {} is functional empty non proper V23() V24() V25() V27() V28() V29() finite V34() cardinal {} -element FinSequence-membered V57() integer ext-real V128() Element of bool {}
({}) is Relation-like [: the carrier of (),(bool {}):] -defined bool {} -valued Function-like V18([: the carrier of (),(bool {}):], bool {}) Element of bool [:[: the carrier of (),(bool {}):],(bool {}):]
[: the carrier of (),(bool {}):] is non empty set
[:[: the carrier of (),(bool {}):],(bool {}):] is non empty set
bool [:[: the carrier of (),(bool {}):],(bool {}):] is non empty set
VectSpStr(# (bool {}),({}),({} {}),({}) #) is non empty strict VectSpStr over ()
dim ({}) is V23() V24() V25() V29() finite cardinal V57() integer ext-real V128() set
[#] ({}) is non empty non proper Element of bool the carrier of ({})
the carrier of ({}) is non empty set
bool the carrier of ({}) is non empty set
card ([#] ({})) is non empty V23() V24() V25() cardinal set