:: MOD_3 semantic presentation

REAL is set
bool REAL is non empty set

bool NAT is non empty set
bool NAT is non empty set
{} is set

1 is non empty set
2 is non empty set
3 is non empty set

the carrier of R is non empty set
0. R is V47(R) Element of the carrier of R
V is Element of the carrier of R
- V is Element of the carrier of R
- (- V) is Element of the carrier of R

0. R is V47(R) Element of the carrier of R
the carrier of R is non empty non trivial set
1. R is V47(R) Element of the carrier of R
- (1. R) is Element of the carrier of R
- (- (1. R)) is Element of the carrier of R

the carrier of R is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set

Carrier A is finite Element of bool the carrier of V
0. R is V47(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set
Sum A is Element of the carrier of V
B is finite Element of bool the carrier of V
B \ () is finite Element of bool the carrier of V

rng c6 is finite set

Sum (A (#) c6) is Element of the carrier of V

rng v is finite set

rng l is finite set
x is set

dom l is finite set
l /. x is Element of the carrier of V
l . x is set
dom (A (#) l) is finite set
(A (#) l) . x is set
A . (l /. x) is Element of the carrier of R
(A . (l /. x)) * (l /. x) is Element of the carrier of V
(0. R) * (l /. x) is Element of the carrier of V
Sum (A (#) l) is Element of the carrier of V
Sum l is Element of the carrier of V
(0. R) * (Sum l) is Element of the carrier of V
0. V is V47(V) Element of the carrier of V

rng (c6 ^ l) is finite set

Sum (A (#) (c6 ^ l)) is Element of the carrier of V
(A (#) c6) ^ (A (#) l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((A (#) c6) ^ (A (#) l)) is Element of the carrier of V
(Sum (A (#) c6)) + (0. V) is Element of the carrier of V
() \/ (B \ ()) is finite Element of bool the carrier of V

the carrier of R is non empty set

the carrier of V is non empty set

Sum A is Element of the carrier of V
B is Element of the carrier of R

Sum (B * A) is Element of the carrier of V
B * (Sum A) is Element of the carrier of V
Carrier (B * A) is finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. R is V47(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not (B * A) . b1 = 0. R } is set
Carrier A is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set

rng c6 is finite set

Sum ((B * A) (#) c6) is Element of the carrier of V

dom c6 is finite set
Seg (len ((B * A) (#) c6)) is finite V38( len ((B * A) (#) c6)) Element of bool NAT

dom ((B * A) (#) c6) is finite set
f is Element of the carrier of V
(A (#) c6) . x is set
c6 /. x is Element of the carrier of V
c6 . x is set
((B * A) (#) c6) . x is set
(B * A) . (c6 /. x) is Element of the carrier of R
((B * A) . (c6 /. x)) * (c6 /. x) is Element of the carrier of V
A . (c6 /. x) is Element of the carrier of R
B * (A . (c6 /. x)) is Element of the carrier of R
(B * (A . (c6 /. x))) * (c6 /. x) is Element of the carrier of V
(A . (c6 /. x)) * (c6 /. x) is Element of the carrier of V
B * ((A . (c6 /. x)) * (c6 /. x)) is Element of the carrier of V
B * f is Element of the carrier of V
Sum (A (#) c6) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
the carrier of R is non empty set
A is Element of bool the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A : verum } is set
B is set

Sum c6 is Element of the carrier of V

B is Element of bool the carrier of V
v is Element of the carrier of V
l is Element of the carrier of V
v + l is Element of the carrier of V

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

Sum f is Element of the carrier of V
v is Element of the carrier of R
l is Element of the carrier of V
v * l is Element of the carrier of V

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

Sum c6 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V

the carrier of B is non empty set

the carrier of B is non empty set
R is set

the carrier of V is non empty set

the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A

the carrier of (V,A,B) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set

Sum B is Element of the carrier of A
{ (Sum b1) where b1 is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set
the carrier of (V,A,B) is non empty set
R is set

the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A

0. V is V47(V) Element of the carrier of V
the carrier of V is non empty set
[: the carrier of A, the carrier of V:] is non empty set
bool [: the carrier of A, the carrier of V:] is non empty set
B is Element of the carrier of A
1. V is Element of the carrier of V
c6 is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of V:]
c6 . B is Element of the carrier of V
Funcs ( the carrier of A, the carrier of V) is non empty FUNCTION_DOMAIN of the carrier of A, the carrier of V
v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of Funcs ( the carrier of A, the carrier of V)
{B} is finite Element of bool the carrier of A
l is finite Element of bool the carrier of A
x is Element of the carrier of A
v . x is Element of the carrier of V
x is finite Element of bool the carrier of A

Carrier l is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not l . b1 = 0. V } is set
{B} is finite Element of bool the carrier of A
x is set
f is Element of the carrier of A
l . f is Element of the carrier of V

Sum x is Element of the carrier of A
(1. V) * B is Element of the carrier of A
Carrier x is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not x . b1 = 0. V } is set

Sum f is Element of the carrier of A

the carrier of V is non empty set

bool the carrier of V is non empty set

B is Element of the carrier of V
the carrier of (R,V,({} the carrier of V)) is non empty set
the carrier of R is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V47(V) Element of the carrier of V

Sum B is Element of the carrier of V
0. V is V47(V) Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V
{(0. V)} is finite Element of bool the carrier of V
A is Element of bool the carrier of V

B is set
the Element of A is Element of A
B is set

0. R is V47(R) Element of the carrier of R
the carrier of R is non empty set
1. R is Element of the carrier of R

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

the carrier of B is non empty set
B is Element of the carrier of V

Sum c6 is Element of the carrier of V

0. R is V47(R) Element of the carrier of R
the carrier of R is non empty set
1. R is Element of the carrier of R

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]
[: the carrier of R, the carrier of V:] is non empty set
[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R
the carrier of () is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V

B is Element of the carrier of V
the carrier of R is non empty set

Sum c6 is Element of the carrier of V

Sum v is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V
A \/ B is Element of bool the carrier of V

0. R is V47(R) Element of the carrier of R
the carrier of R is non empty set
B is Element of the carrier of V

Sum c6 is Element of the carrier of V
Carrier c6 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c6 . b1 = 0. R } is set
(Carrier c6) \ A is finite Element of bool the carrier of V
(Carrier c6) /\ A is finite Element of bool the carrier of V
x is set
c6 . x is set
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
f is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
f . f is Element of the carrier of R
f is set
c6 . f is set
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
f is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
f . f is Element of the carrier of R
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
f is finite Element of bool the carrier of V
f is set
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
g is Element of the carrier of V
f . g is Element of the carrier of R

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. R } is set
g is set
g is Element of the carrier of V
g . g is Element of the carrier of R
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
x is finite Element of bool the carrier of V
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
u is Element of the carrier of V
g . u is Element of the carrier of R

Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0. R } is set
f is set
v is Element of the carrier of V
u . v is Element of the carrier of R

v is Element of the carrier of V
c6 . v is Element of the carrier of R
(f + g) . v is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(c6 . v) + (g . v) is Element of the carrier of R
(c6 . v) + (0. R) is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(0. R) + (g . v) is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(0. R) + (g . v) is Element of the carrier of R
(0. R) + (0. R) is Element of the carrier of R
Sum f is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum f) + (Sum g) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V
A /\ B is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of ((0). V) is non empty set
bool the carrier of ((0). V) is non empty set
the carrier of V is non empty set

bool the carrier of V is non empty set
B is Element of bool the carrier of ((0). V)

the carrier of R is non empty non trivial set
0. R is V47(R) Element of the carrier of R
1. R is V47(R) Element of the carrier of R
V is Element of the carrier of R
V " is Element of the carrier of R
(V ") * V is Element of the carrier of R

the carrier of A is non empty set
B is Element of the carrier of A
V * B is Element of the carrier of A
(V ") * (V * B) is Element of the carrier of A
(1. R) * B is Element of the carrier of A
((V ") * V) * B is Element of the carrier of A

the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
{A} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. R is V47(R) Element of the carrier of R
the carrier of R is non empty non trivial set
1. R is V47(R) Element of the carrier of R

Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0. R } is set
B . A is Element of the carrier of R
(B . A) * A is Element of the carrier of V

the carrier of R is non empty non trivial set

the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. R is V47(R) Element of the carrier of R
1. R is V47(R) Element of the carrier of R
B is Element of the carrier of R
B * B is Element of the carrier of V
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
- (1. R) is Element of the carrier of R
c6 is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
c6 . A is Element of the carrier of R
c6 . B is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
l is Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
v . l is Element of the carrier of R

Carrier l is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
x is set
f is Element of the carrier of V
l . f is Element of the carrier of R

Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0. R } is set
Sum x is Element of the carrier of V
(- (1. R)) * (B * B) is Element of the carrier of V
((- (1. R)) * (B * B)) + (B * B) is Element of the carrier of V
- (B * B) is Element of the carrier of V
(- (B * B)) + (B * B) is Element of the carrier of V
(1. R) * B is Element of the carrier of V

Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0. R } is set
B . A is Element of the carrier of R
(B . A) * A is Element of the carrier of V
B . B is Element of the carrier of R
(B . B) * B is Element of the carrier of V
((B . A) * A) + ((B . B) * B) is Element of the carrier of V
the Element of Carrier B is Element of Carrier B
(B . A) " is Element of the carrier of R
((B . A) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . A) ") * ((B . A) * A) is Element of the carrier of V
((B . A) ") * ((B . B) * B) is Element of the carrier of V
(((B . A) ") * ((B . A) * A)) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . A) is Element of the carrier of R
(((B . A) ") * (B . A)) * A is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . B) is Element of the carrier of R
(((B . A) ") * (B . B)) * B is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(1. R) * A is Element of the carrier of V
((1. R) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
A + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
- ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
- (1. R) is Element of the carrier of R
(- (1. R)) * ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(- (1. R)) * (((B . A) ") * (B . B)) is Element of the carrier of R
((- (1. R)) * (((B . A) ") * (B . B))) * B is Element of the carrier of V
(B . B) " is Element of the carrier of R
((B . B) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . B) ") * ((B . A) * A) is Element of the carrier of V
((B . B) ") * ((B . B) * B) is Element of the carrier of V
(((B . B) ") * ((B . A) * A)) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((B . B) ") * (B . A) is Element of the carrier of R
(((B . B) ") * (B . A)) * A is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + ((1. R) * B) is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + B is Element of the carrier of V
(0. R) * A is Element of the carrier of V
((0. R) * A) + B is Element of the carrier of V
(0. V) + B is Element of the carrier of V
v is Element of the carrier of V
B . v is Element of the carrier of R

the carrier of R is non empty non trivial set
0. R is V47(R) Element of the carrier of R

the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is Element of the carrier of R
B * A is Element of the carrier of V
c6 is Element of the carrier of R
c6 * B is Element of the carrier of V
(B * A) + (c6 * B) is Element of the carrier of V
B " is Element of the carrier of R
(B ") * ((B * A) + (c6 * B)) is Element of the carrier of V
(B ") * (B * A) is Element of the carrier of V
(B ") * (c6 * B) is Element of the carrier of V
((B ") * (B * A)) + ((B ") * (c6 * B)) is Element of the carrier of V
(B ") * B is Element of the carrier of R
((B ") * B) * A is Element of the carrier of V
(((B ") * B) * A) + ((B ") * (c6 * B)) is Element of the carrier of V
(B ") * c6 is Element of the carrier of R
((B ") * c6) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c6) * B) is Element of the carrier of V
1. R is V47(R) Element of the carrier of R
(1. R) * A is Element of the carrier of V
((1. R) * A) + (((B ") * c6) * B) is Element of the carrier of V
A + (((B ") * c6) * B) is Element of the carrier of V
- (((B ") * c6) * B) is Element of the carrier of V
- (1. R) is Element of the carrier of R
(- (1. R)) * (((B ") * c6) * B) is Element of the carrier of V
(- (1. R)) * ((B ") * c6) is Element of the carrier of R
((- (1. R)) * ((B ") * c6)) * B is Element of the carrier of V
c6 " is Element of the carrier of R
(c6 ") * ((B * A) + (c6 * B)) is Element of the carrier of V
(c6 ") * (B * A) is Element of the carrier of V
(c6 ") * (c6 * B) is Element of the carrier of V
((c6 ") * (B * A)) + ((c6 ") * (c6 * B)) is Element of the carrier of V
(c6 ") * B is Element of the carrier of R
((c6 ") * B) * A is Element of the carrier of V
(((c6 ") * B) * A) + ((c6 ") * (c6 * B)) is Element of the carrier of V
1. R is V47(R) Element of the carrier of R
(1. R) * B is Element of the carrier of V
(((c6 ") * B) * A) + ((1. R) * B) is Element of the carrier of V
(((c6 ") * B) * A) + B is Element of the carrier of V
- (((c6 ") * B) * A) is Element of the carrier of V
- (1. R) is Element of the carrier of R
(- (1. R)) * (((c6 ") * B) * A) is Element of the carrier of V
(- (1. R)) * ((c6 ") * B) is Element of the carrier of R
((- (1. R)) * ((c6 ") * B)) * A is Element of the carrier of V
B is Element of the carrier of R
B * B is Element of the carrier of V
(0. V) + (B * B) is Element of the carrier of V
A - (B * B) is Element of the carrier of V
- B is Element of the carrier of R
(- B) * B is Element of the carrier of V
A + ((- B) * B) is Element of the carrier of V
1. R is V47(R) Element of the carrier of R
(1. R) * A is Element of the carrier of V
((1. R) * A) + ((- B) * B) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
(0. R) * A is Element of the carrier of V
((0. R) * A) + (0. V) is Element of the carrier of V
(1. R) * B is Element of the carrier of V
((0. R) * A) + ((1. R) * B) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
B is set
B is set
union B is set
v is set
l is set
v is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in B ) } is set
the carrier of R is non empty non trivial set

Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
0. R is V47(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set

dom x is set
rng x is set
f is non empty set
union f is set

g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is set
g is set

g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union () is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is Element of bool the carrier of V
the Element of B is Element of B
x is Element of bool the carrier of V
B is set
c6 is Element of bool the carrier of V

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]
the carrier of R is non empty non trivial set
[: the carrier of R, the carrier of V:] is non empty set
[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R

v is Element of the carrier of V
{v} is finite Element of bool the carrier of V
c6 \/ {v} is Element of bool the carrier of V

Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
0. R is V47(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
l . v is Element of the carrier of R
- (l . v) is Element of the carrier of R
(- (l . v)) " is Element of the carrier of R
(- (l . v)) * v is Element of the carrier of V
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
1. R is V47(R) Element of the carrier of R
(1. R) * v is Element of the carrier of V
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
x . v is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
f is Element of the carrier of V
() \ {v} is finite Element of bool the carrier of V
l . f is Element of the carrier of R
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
f . f is Element of the carrier of R

Carrier f is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not f . b1 = 0. R } is set
f is set
g is Element of the carrier of V
f . g is Element of the carrier of R
l . g is Element of the carrier of R
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
g . v is Element of the carrier of R
g is Element of the carrier of V
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
g . g is Element of the carrier of R

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. R } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of R

- (1. R) is Element of the carrier of R
(- (1. R)) * g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is Element of the carrier of R
l . u is Element of the carrier of R
f . u is Element of the carrier of R
g . u is Element of the carrier of R
(f . u) - (g . u) is Element of the carrier of R
- (- (l . v)) is Element of the carrier of R
(0. R) + (- (- (l . v))) is Element of the carrier of R
(l . v) + (0. R) is Element of the carrier of R
f . u is Element of the carrier of R
g . u is Element of the carrier of R
(f . u) - (g . u) is Element of the carrier of R
(l . u) - (g . u) is Element of the carrier of R
(l . u) - (0. R) is Element of the carrier of R
Sum f is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
x is set

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

0. R is V47(R) Element of the carrier of R
the carrier of R is non empty non trivial set
1. R is V47(R) Element of the carrier of R
B is set
B is set
union B is set
v is set
l is set
v is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in B ) } is set

Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set

dom x is set
rng x is set
f is non empty set
union f is set

g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is set
g is set

g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union () is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is Element of bool the carrier of V
l is set
x is set
f is Element of bool the carrier of V

B is set
c6 is Element of bool the carrier of V

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]
[: the carrier of R, the carrier of V:] is non empty set
[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R
the carrier of (R,V,c6) is non empty set
l is Element of the carrier of V

Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0. R } is set
f is set
f is Element of the carrier of V
v is Element of bool the carrier of V

Sum f is Element of the carrier of V

v is Element of the carrier of V
v is Element of the carrier of V
{v} is finite Element of bool the carrier of V
c6 \/ {v} is Element of bool the carrier of V

Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
l . v is Element of the carrier of R
- (l . v) is Element of the carrier of R
(- (l . v)) " is Element of the carrier of R
(- (l . v)) * v is Element of the carrier of V
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
(1. R) * v is Element of the carrier of V
[: the carrier of V, the carrier of R:] is non empty set
bool [: the carrier of V, the carrier of R:] is non empty set
x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
x . v is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
f is Element of the carrier of V
() \ {v} is finite Element of bool the carrier of V
l . f is Element of the carrier of R
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
f . f is Element of the carrier of R

Carrier f is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not f . b1 = 0. R } is set
f is set
g is Element of the carrier of V
f . g is Element of the carrier of R
l . g is Element of the carrier of R
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]
g . v is Element of the carrier of R
g is Element of the carrier of V
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
g . g is Element of the carrier of R

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. R } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of R

- (1. R) is Element of the carrier of R
(- (1. R)) * g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is Element of the carrier of R
l . u is Element of the carrier of R
f . u is Element of the carrier of R
g . u is Element of the carrier of R
(f . u) - (g . u) is Element of the carrier of R
- (- (l . v)) is Element of the carrier of R
(0. R) + (- (- (l . v))) is Element of the carrier of R
(l . v) + (0. R) is Element of the carrier of R
f . u is Element of the carrier of R
g . u is Element of the carrier of R
(f . u) - (g . u) is Element of the carrier of R
(l . u) - (g . u) is Element of the carrier of R
(l . u) - (0. R) is Element of the carrier of R
Sum f is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
x is set

the carrier of V is non empty set
bool the carrier of V is non empty set

A is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
B is Element of bool the carrier of V
B is (R,V)

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V
B is (R,V)