NAT is non empty V18() V19() V20() Element of K19(REAL)
REAL is set
K19(REAL) is non empty set
NAT is non empty V18() V19() V20() set
K19(NAT) is non empty set
K19(NAT) is non empty set
{} is Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set
the Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set is Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set
1 is non empty set
R is non empty doubleLoopStr
V is non empty VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
R is non empty doubleLoopStr
V is non empty VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Element of K19( the carrier of V)
the carrier of R is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum v is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
Carrier v is finite Element of K19( the carrier of V)
0. R is V49(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not v . b1 = 0. R } is set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B
Carrier l is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty set
1. R is Element of the carrier of R
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
0. V is V49(V) Element of the carrier of V
A is Element of K19( the carrier of V)
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
B . (0. 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
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)
{(0. V)} is non empty finite Element of K19( the carrier of V)
l is non empty finite Element of K19( the carrier of V)
D is Element of the carrier of V
v . D is Element of the carrier of R
D is finite Element of K19( the carrier of V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Carrier l is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
{(0. V)} is non empty finite Element of K19( the carrier of V)
D is set
C is Element of the carrier of V
l . C is Element of the carrier of R
D is set
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum D is Element of the carrier of V
D . (0. V) is Element of the carrier of R
(D . (0. V)) * (0. V) is Element of the carrier of V
R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper V18() V19() V20() V22() V23() V24() finite V29() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V
Sum A is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
Carrier A is finite Element of K19( the carrier of V)
0. R is V49(R) Element of the carrier of R
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set
R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty set
1. R is Element of the carrier of R
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
0. V is V49(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 non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty set
1. R is Element of the carrier of R
A is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
{A,(0. V)} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{(0. V),A} is non empty finite Element of K19( the carrier of V)
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
the carrier of R is non empty V12() set
0. R is V49(R) Element of the carrier of R
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Carrier A is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set
B is Element of the carrier of R
B * A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Carrier (B * A) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not (B * A) . b1 = 0. R } is set
D is set
C is Element of the carrier of V
(B * A) . C is Element of the carrier of R
A . C is Element of the carrier of R
B * (A . C) is Element of the carrier of R
D is set
C is Element of the carrier of V
A . C is Element of the carrier of R
(B * A) . C is Element of the carrier of R
B * (A . C) is Element of the carrier of R
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
the carrier of R is non empty V12() set
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Sum A is Element of the carrier of V
B is Element of the carrier of R
B * A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Sum (B * A) is Element of the carrier of V
B * (Sum A) is Element of the carrier of V
0. R is V49(R) Element of the carrier of R
Carrier (B * A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b1 where b1 is Element of the carrier of V : not (B * A) . b1 = 0. R } is set
Carrier A is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set
l is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng l is set
A (#) l is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum (A (#) l) is Element of the carrier of V
C is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng C is set
(B * A) (#) C is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((B * A) (#) C) is Element of the carrier of V
len l is V18() V19() V20() V24() Element of NAT
len C is V18() V19() V20() V24() Element of NAT
f is Relation-like Function-like FinSequence-like set
len f is V18() V19() V20() V24() Element of NAT
dom f is Element of K19(NAT)
Seg (len C) is Element of K19(NAT)
dom C is Element of K19(NAT)
f is set
dom l is Element of K19(NAT)
f is V18() V19() V20() V24() Element of NAT
l . f is set
f . f is set
C . (f . f) is set
C <- (l . f) is set
C . (C <- (l . f)) is set
l . f is set
f . f is set
C . (f . f) is set
rng f is set
f is set
f is set
f . f is set
g is V18() V19() V20() V24() Element of NAT
l . g is set
f . g is set
C <- (l . g) is set
f is set
f . f is set
f (#) C is Relation-like Function-like set
C " is Relation-like Function-like set
l (#) (C ") is Relation-like Function-like set
f is set
dom (C ") is set
rng (l (#) (C ")) is set
rng (C ") is set
C (#) (C ") is Relation-like Function-like set
f (#) (C (#) (C ")) is Relation-like Function-like set
id (dom C) is Relation-like dom C -defined dom C -valued Function-like one-to-one total Element of K19(K20((dom C),(dom C)))
K20((dom C),(dom C)) is set
K19(K20((dom C),(dom C))) is non empty set
f (#) (id (dom C)) is Relation-like Function-like set
K20((dom C),(dom C)) is set
K19(K20((dom C),(dom C))) is non empty set
len ((B * A) (#) C) is V18() V19() V20() V24() Element of NAT
dom ((B * A) (#) C) is Element of K19(NAT)
K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))) is set
K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C)))) is non empty set
f is Relation-like dom C -defined dom C -valued Function-like quasi_total Element of K19(K20((dom C),(dom C)))
f is Relation-like dom ((B * A) (#) C) -defined dom ((B * A) (#) C) -valued Function-like quasi_total Element of K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))))
((B * A) (#) C) * f is Relation-like dom ((B * A) (#) C) -defined the carrier of V -valued Function-like Element of K19(K20((dom ((B * A) (#) C)), the carrier of V))
K20((dom ((B * A) (#) C)), the carrier of V) is set
K19(K20((dom ((B * A) (#) C)), the carrier of V)) is non empty set
g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
g is Relation-like dom ((B * A) (#) C) -defined dom ((B * A) (#) C) -valued Function-like quasi_total bijective Element of K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))))
((B * A) (#) C) * g is Relation-like dom ((B * A) (#) C) -defined the carrier of V -valued Function-like Element of K19(K20((dom ((B * A) (#) C)), the carrier of V))
len g is V18() V19() V20() V24() Element of NAT
len (A (#) l) is V18() V19() V20() V24() Element of NAT
g is V18() V19() V20() V24() Element of NAT
dom g is Element of K19(NAT)
g is Element of the carrier of V
(A (#) l) . g is set
Seg (len (A (#) l)) is Element of K19(NAT)
dom g is set
l . g is set
C <- (l . g) is set
l /. g is Element of the carrier of V
g . g is set
C . (g . g) is set
v is V18() V19() V20() V24() Element of NAT
C . v is set
C /. v is Element of the carrier of V
dom (A (#) l) is Element of K19(NAT)
Seg (len ((B * A) (#) C)) is Element of K19(NAT)
g . g is set
((B * A) (#) C) . (g . g) is set
((B * A) (#) C) . (C <- (l . g)) is set
(B * A) . (C /. v) is Element of the carrier of R
((B * A) . (C /. v)) * (C /. v) is Element of the carrier of V
A . (C /. v) is Element of the carrier of R
B * (A . (C /. v)) is Element of the carrier of R
(B * (A . (C /. v))) * (C /. v) is Element of the carrier of V
(A . (C /. v)) * (C /. v) is Element of the carrier of V
B * ((A . (C /. v)) * (C /. v)) is Element of the carrier of V
B * g is Element of the carrier of V
Sum g is Element of the carrier of V
0. R is V49(R) Element of the carrier of R
ZeroLC V is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
Sum (ZeroLC V) is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
0. R is V49(R) Element of the carrier of R
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
the carrier of R is non empty V12() set
A is Element of K19( 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
v is set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum l is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
v is Element of K19( the carrier of V)
D is Element of the carrier of V
C is Element of the carrier of V
D + C 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 Linear_Combination of A
Sum 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 Linear_Combination of A
Sum f is Element of the carrier of V
f + f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
D is Element of the carrier of R
C is Element of the carrier of V
D * C 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 Linear_Combination of A
Sum f is Element of the carrier of V
D * f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum l is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
B is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
the carrier of B is non empty set
v is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
the carrier of v is non empty set
R is set
V is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
the carrier of V is non empty V12() set
A is non empty right_complementable V105(V) V106(V) V107(V) V108(V) V112() V113() V114() VectSpStr over V
the carrier of A is non empty set
K19( the carrier of A) is non empty set
B is Element of K19( the carrier of A)
(V,A,B) is non empty right_complementable strict V105(V) V106(V) V107(V) V108(V) V112() V113() V114() Subspace 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
v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B
Sum v 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
V is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
A is non empty right_complementable V105(V) V106(V) V107(V) V108(V) V112() V113() V114() VectSpStr over V
the carrier of A is non empty set
K19( the carrier of A) is non empty set
B is Element of K19( the carrier of A)
(V,A,B) is non empty right_complementable strict V105(V) V106(V) V107(V) V108(V) V112() V113() V114() Subspace of A
0. V is V49(V) Element of the carrier of V
the carrier of V is non empty V12() set
K20( the carrier of A, the carrier of V) is non empty set
K19(K20( the carrier of A, the carrier of V)) is non empty set
v is Element of the carrier of A
1. V is V49(V) Element of the carrier of V
l is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of K19(K20( the carrier of A, the carrier of V))
l . v 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
D 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)
{v} is non empty finite Element of K19( the carrier of A)
C is non empty finite Element of K19( the carrier of A)
f is Element of the carrier of A
D . f is Element of the carrier of V
f is finite Element of K19( the carrier of A)
C is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of A
Carrier C is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not C . b1 = 0. V } is set
{v} is non empty finite Element of K19( the carrier of A)
f is set
f is Element of the carrier of A
C . f is Element of the carrier of V
f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of {v}
Sum f is Element of the carrier of A
(1. V) * v is Element of the carrier of A
Carrier f is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not f . b1 = 0. V } is set
f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B
Sum f is Element of the carrier of A
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper V18() V19() V20() V22() V23() V24() finite V29() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V,({} the carrier of V)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(0). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
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 V12() 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 V49(V) Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V
Sum v is Element of the carrier of V
0. V is V49(V) Element of the carrier of V
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
(0). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
0. V is V49(V) Element of the carrier of V
{(0. V)} is non empty finite Element of K19( the carrier of V)
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is set
the Element of A is Element of A
v is set
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty V12() set
1. R is V49(R) Element of the carrier of R
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
the carrier of B is non empty set
v is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum l is Element of the carrier of V
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty V12() set
1. R is V49(R) Element of the carrier of R
V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(Omega). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
the addF of V is Relation-like K20( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of V, the carrier of V), the carrier of V))
K20( the carrier of V, the carrier of V) is non empty set
K20(K20( the carrier of V, the carrier of V), the carrier of V) is non empty set
K19(K20(K20( 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 K20( the carrier of R, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of R, the carrier of V), the carrier of V))
K20( the carrier of R, the carrier of V) is non empty set
K20(K20( the carrier of R, the carrier of V), the carrier of V) is non empty set
K19(K20(K20( 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
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is Element of K19( the carrier of V)
(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
v is Element of the carrier of V
the carrier of R is non empty V12() set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum l is Element of the carrier of V
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B
Sum D is Element of the carrier of V
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is Element of K19( the carrier of V)
(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is Element of K19( the carrier of V)
A \/ B is Element of K19( the carrier of V)
(R,V,(A \/ B)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(R,V,A) + (R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
0. R is V49(R) Element of the carrier of R
the carrier of R is non empty V12() set
v is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A \/ B
Sum l is Element of the carrier of V
Carrier l is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. R } is set
(Carrier l) \ A is finite Element of K19( the carrier of V)
(Carrier l) /\ A is finite Element of K19( the carrier of V)
f is set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( 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 K19(K20( the carrier of V, the carrier of R))
f . f is Element of the carrier of R
l . f is set
f is set
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, 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 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 is Element of the carrier of V
f . 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 Linear_Combination of V
Carrier f is finite Element of K19( 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
g is set
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 K19(K20( the carrier of V, the carrier of R))
g . g is Element of the carrier of R
l . g is set
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
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 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 Linear_Combination of V
Carrier g is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. R } is set
g is set
v is Element of the carrier of V
g . v 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 Linear_Combination of A
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B
f + g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V
v is Element of the carrier of V
l . 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
(l . v) + (g . v) is Element of the carrier of R
(l . 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
R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr
V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
B is Element of K19( the carrier of V)
A /\ B is Element of K19( the carrier of V)
(R,V,(A /\ B)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V
(R,V,A) /\ (R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V