:: RANKNULL semantic presentation

REAL is set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is non empty set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set
K6(NAT) is non empty V2() non finite set
K6(NAT) is non empty V2() non finite set
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of NAT
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set
the empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set
1 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
2 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
K223(0,1,2) is non empty finite set
K7(K223(0,1,2),K223(0,1,2)) is non empty Relation-like finite set
K7(K7(K223(0,1,2),K223(0,1,2)),K223(0,1,2)) is non empty Relation-like finite set
K6(K7(K7(K223(0,1,2),K223(0,1,2)),K223(0,1,2))) is non empty finite V38() set
K6(K7(K223(0,1,2),K223(0,1,2))) is non empty finite V38() set
COMPLEX is set
RAT is set
INT is set
K7(NAT,REAL) is Relation-like set
K6(K7(NAT,REAL)) is non empty set
3 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
V is Relation-like Function-like set
F is Relation-like Function-like set
rng V is set
F | (rng V) is Relation-like Function-like set
dom F is set
V (#) F is Relation-like Function-like set
dom (V (#) F) is set
dom V is set
T is set
T is set
V . T is set
T is set
A is set
(V (#) F) . T is set
(V (#) F) . A is set
V . T is set
F . (V . T) is set
V . A is set
F . (V . A) is set
dom (F | (rng V)) is set
(F | (rng V)) . (V . T) is set
(F | (rng V)) . (V . A) is set
F is Relation-like Function-like set
V is set
W is set
F | W is Relation-like Function-like set
F | V is Relation-like Function-like set
(F | W) | V is Relation-like Function-like set
F is 1-sorted
the carrier of F is set
K6( the carrier of F) is non empty set
V is Element of K6( the carrier of F)
W is Element of K6( the carrier of F)
T is set
A is Element of the carrier of F
T is Element of the carrier of F
A is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is finite Element of K6( the carrier of V)
T is Basis of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
[#] V is non empty non proper Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
FuncZero (([#] V),W) is Relation-like [#] V -defined the carrier of W -valued Function-like quasi_total Element of Funcs (([#] V), the carrier of W)
Funcs (([#] V), the carrier of W) is non empty FUNCTION_DOMAIN of [#] V, the carrier of W
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
([#] V) --> (0. W) is non empty Relation-like [#] V -defined the carrier of W -valued Function-like constant total quasi_total Element of K6(K7(([#] V), the carrier of W))
K7(([#] V), the carrier of W) is non empty Relation-like set
K6(K7(([#] V), the carrier of W)) is non empty set
{(0. W)} is non empty V2() finite 1 -element set
K7(([#] V),{(0. W)}) is non empty Relation-like set
A is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total Element of K6(K7( the carrier of V, the carrier of W))
A9 is Element of the carrier of V
B is Element of the carrier of V
A9 + B is Element of the carrier of V
A . (A9 + B) is Element of the carrier of W
A . A9 is Element of the carrier of W
A . B is Element of the carrier of W
(A . A9) + (A . B) is Element of the carrier of W
the carrier of F is non empty V2() set
A9 is Element of the carrier of F
B is Element of the carrier of V
A9 * B is Element of the carrier of V
A . (A9 * B) is Element of the carrier of W
A . B is Element of the carrier of W
A9 * (A . B) is Element of the carrier of W
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
[#] V is non empty non proper Element of K6( the carrier of V)
the carrier of V is non empty set
K6( the carrier of V) is non empty set
the Basis of V is Basis of V
T is finite Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
[#] V is non empty non proper Element of K6( the carrier of V)
the carrier of V is non empty set
K6( the carrier of V) is non empty set
card ([#] V) is non empty V4() V5() V6() cardinal set
dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty V2() finite 1 -element Element of K6( the carrier of V)
W is set
{W} is non empty V2() finite 1 -element set
(Omega). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
the U5 of V is Relation-like K7( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of V, the carrier of V), the carrier of V))
K7( the carrier of V, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of V, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the lmult of V is Relation-like K7( the carrier of F, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of V), the carrier of V))
the carrier of F is non empty V2() set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of F, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( the carrier of F, the carrier of V), the carrier of V)) is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is strict VectSpStr over F
(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
[#] V is non empty non proper Element of K6( the carrier of V)
the carrier of V is non empty set
K6( the carrier of V) is non empty set
card ([#] V) is non empty V4() V5() V6() cardinal set
dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
T is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of T is non empty set
0. T is V55(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(Omega). T is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T
the U5 of T is Relation-like K7( the carrier of T, the carrier of T) -defined the carrier of T -valued Function-like quasi_total Element of K6(K7(K7( the carrier of T, the carrier of T), the carrier of T))
K7( the carrier of T, the carrier of T) is non empty Relation-like set
K7(K7( the carrier of T, the carrier of T), the carrier of T) is non empty Relation-like set
K6(K7(K7( the carrier of T, the carrier of T), the carrier of T)) is non empty set
the lmult of T is Relation-like K7( the carrier of F, the carrier of T) -defined the carrier of T -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of T), the carrier of T))
the carrier of F is non empty V2() set
K7( the carrier of F, the carrier of T) is non empty Relation-like set
K7(K7( the carrier of F, the carrier of T), the carrier of T) is non empty Relation-like set
K6(K7(K7( the carrier of F, the carrier of T), the carrier of T)) is non empty set
VectSpStr(# the carrier of T, the U5 of T, the ZeroF of T, the lmult of T #) is strict VectSpStr over F
[#] T is non empty non proper Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
A is set
A9 is set
{A,A9} is non empty finite set
B is Element of the carrier of T
{B} is non empty V2() finite 1 -element Element of K6( the carrier of T)
Lin {B} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T
X is Element of the carrier of T
0. (Lin {B}) is V55( Lin {B}) Element of the carrier of (Lin {B})
the carrier of (Lin {B}) is non empty set
the ZeroF of (Lin {B}) is Element of the carrier of (Lin {B})
B is Element of the carrier of T
B is Element of the carrier of T
B is Element of the carrier of T
{B} is non empty V2() finite 1 -element Element of K6( the carrier of T)
Lin {B} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T
X is Element of the carrier of T
0. (Lin {B}) is V55( Lin {B}) Element of the carrier of (Lin {B})
the carrier of (Lin {B}) is non empty set
the ZeroF of (Lin {B}) is Element of the carrier of (Lin {B})
B is Element of the carrier of T
B is Element of the carrier of T
A is Element of the carrier of T
{A} is non empty V2() finite 1 -element Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
Lin {A} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
F is non empty 1-sorted
the carrier of F is non empty set
V is non empty 1-sorted
the carrier of V is non empty set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of F, the carrier of V)) is non empty set
[#] F is non empty non proper Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
[#] V is non empty non proper Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))
dom W is Element of K6( the carrier of F)
rng W is set
Funcs (([#] F),([#] V)) is non empty FUNCTION_DOMAIN of [#] F, [#] V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Element of the carrier of W
T . A is Element of the carrier of V
A9 is Element of the carrier of W
T . A9 is Element of the carrier of V
(T . A) - (T . A9) is Element of the carrier of V
- (T . A9) is Element of the carrier of V
K176(V,(T . A),(- (T . A9))) is Element of the carrier of V
A - A9 is Element of the carrier of W
- A9 is Element of the carrier of W
K176(W,A,(- A9)) is Element of the carrier of W
T . (A - A9) is Element of the carrier of V
1. F is V55(F) Element of the carrier of F
the carrier of F is non empty V2() set
the OneF of F is Element of the carrier of F
- (1. F) is Element of the carrier of F
(- (1. F)) * A9 is Element of the carrier of W
T . ((- (1. F)) * A9) is Element of the carrier of V
(- (1. F)) * (T . A9) is Element of the carrier of V
T . (- A9) is Element of the carrier of V
(T . A) + (T . (- A9)) is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
T . (0. V) is Element of the carrier of W
0. F is V55(F) Element of the carrier of F
the carrier of F is non empty V2() set
the ZeroF of F is Element of the carrier of F
(0. F) * (0. V) is Element of the carrier of V
(0. F) * (T . (0. V)) is Element of the carrier of W
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
{ b₁ where b₁ is Element of the carrier of V : T . b₁ = 0. W } is set
[#] V is non empty non proper Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
A9 is set
B is Element of the carrier of V
T . B is Element of the carrier of W
A9 is Element of K6( the carrier of V)
B is Element of the carrier of V
T . B is Element of the carrier of W
B is Element of the carrier of V
T . B is Element of the carrier of W
the carrier of F is non empty V2() set
B is Element of the carrier of V
T . B is Element of the carrier of W
B is Element of the carrier of F
B * B is Element of the carrier of V
T . (B * B) is Element of the carrier of W
B * (0. W) is Element of the carrier of W
B is Element of the carrier of V
B is Element of the carrier of F
B * B is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
T . (0. V) is Element of the carrier of W
B is Element of the carrier of V
B is Element of the carrier of V
T . B is Element of the carrier of W
T . B is Element of the carrier of W
B + B is Element of the carrier of V
T . (B + B) is Element of the carrier of W
(0. W) + (0. W) is Element of the carrier of W
B is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
the carrier of B is non empty set
[#] B is non empty non proper Element of K6( the carrier of B)
K6( the carrier of B) is non empty set
A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
[#] A is non empty non proper Element of K6( the carrier of A)
the carrier of A is non empty set
K6( the carrier of A) is non empty set
A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
[#] A9 is non empty non proper Element of K6( the carrier of A9)
the carrier of A9 is non empty set
K6( the carrier of A9) is non empty set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
A is Element of the carrier of V
T . A is Element of the carrier of W
[#] (F,V,W,T) is non empty non proper Element of K6( the carrier of (F,V,W,T))
the carrier of (F,V,W,T) is non empty set
K6( the carrier of (F,V,W,T)) is non empty set
{ b₁ where b₁ is Element of the carrier of V : T . b₁ = 0. W } is set
A9 is Element of the carrier of V
T . A9 is Element of the carrier of W
{ b₁ where b₁ is Element of the carrier of V : T . b₁ = 0. W } is set
[#] (F,V,W,T) is non empty non proper Element of K6( the carrier of (F,V,W,T))
the carrier of (F,V,W,T) is non empty set
K6( the carrier of (F,V,W,T)) is non empty set
F is non empty 1-sorted
the carrier of F is non empty set
V is non empty 1-sorted
the carrier of V is non empty set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of F, the carrier of V)) is non empty set
K6( the carrier of F) is non empty set
W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))
T is Element of K6( the carrier of F)
W .: T is set
K6( the carrier of V) is non empty set
rng W is set
[#] V is non empty non proper Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
[#] V is non empty non proper Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(V,W,T,([#] V)) is Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
A is Element of K6( the carrier of W)
A9 is Element of the carrier of W
dom T is Element of K6( the carrier of V)
B is set
T . B is set
B is Element of the carrier of V
T . B is Element of the carrier of W
B is Element of the carrier of V
T . B is Element of the carrier of W
dom T is Element of K6( the carrier of V)
A9 is Element of the carrier of W
B is Element of the carrier of W
B is Element of the carrier of V
T . B is Element of the carrier of W
X is Element of the carrier of V
T . X is Element of the carrier of W
A9 + B is Element of the carrier of W
B + X is Element of the carrier of V
T . (B + X) is Element of the carrier of W
the carrier of F is non empty V2() set
B is Element of the carrier of W
B is Element of the carrier of V
T . B is Element of the carrier of W
A9 is Element of the carrier of F
A9 * B is Element of the carrier of V
T . (A9 * B) is Element of the carrier of W
A9 * B is Element of the carrier of W
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
T . (0. V) is Element of the carrier of W
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
the carrier of A9 is non empty set
[#] A9 is non empty non proper Element of K6( the carrier of A9)
K6( the carrier of A9) is non empty set
A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
[#] A is non empty non proper Element of K6( the carrier of A)
the carrier of A is non empty set
K6( the carrier of A) is non empty set
A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
[#] A9 is non empty non proper Element of K6( the carrier of A9)
the carrier of A9 is non empty set
K6( the carrier of A9) is non empty set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
0. F is V55(F) Element of the carrier of F
the carrier of F is non empty V2() set
the ZeroF of F is Element of the carrier of F
(0. F) * (0. W) is Element of the carrier of W
T . (0. W) is Element of the carrier of V
(0. F) * (T . (0. W)) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
the carrier of (F,W,V,T) is non empty set
K6( the carrier of (F,W,V,T)) is non empty set
A is Element of K6( the carrier of W)
(W,V,T,A) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))
[#] W is non empty non proper Element of K6( the carrier of W)
(W,V,T,([#] W)) is Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
A is Element of the carrier of V
the carrier of (F,W,V,T) is non empty set
[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))
K6( the carrier of (F,W,V,T)) is non empty set
[#] W is non empty non proper Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
(W,V,T,([#] W)) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
dom T is Element of K6( the carrier of W)
A9 is Element of the carrier of (F,W,V,T)
B is set
T . B is set
B is Element of the carrier of W
T . B is Element of the carrier of V
dom T is Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
[#] W is non empty non proper Element of K6( the carrier of W)
(W,V,T,([#] W)) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
A9 is Element of the carrier of W
T . A9 is Element of the carrier of V
[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))
the carrier of (F,W,V,T) is non empty set
K6( the carrier of (F,W,V,T)) is non empty set
A9 is Element of the carrier of W
T . A9 is Element of the carrier of V
B is Element of the carrier of W
T . B is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
the carrier of (F,V,W,T) is non empty set
A is Element of the carrier of (F,V,W,T)
T . A is set
A9 is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
(0). W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
the carrier of (F,W,V,T) is non empty set
A is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) Subspace of (F,W,V,T)
A9 is Element of the carrier of (F,W,V,T)
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
T . (0. W) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
dom T is Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
[#] W is non empty non proper Element of K6( the carrier of W)
B is Element of the carrier of W
T . B is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
dim ((0). V) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(Omega). ((0). V) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (0). V
the carrier of ((0). V) is non empty set
the U5 of ((0). V) is Relation-like K7( the carrier of ((0). V), the carrier of ((0). V)) -defined the carrier of ((0). V) -valued Function-like quasi_total Element of K6(K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V)))
K7( the carrier of ((0). V), the carrier of ((0). V)) is non empty Relation-like set
K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V)) is non empty Relation-like set
K6(K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V))) is non empty set
the ZeroF of ((0). V) is Element of the carrier of ((0). V)
the lmult of ((0). V) is Relation-like K7( the carrier of F, the carrier of ((0). V)) -defined the carrier of ((0). V) -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V)))
the carrier of F is non empty V2() set
K7( the carrier of F, the carrier of ((0). V)) is non empty Relation-like set
K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V)) is non empty Relation-like set
K6(K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V))) is non empty set
VectSpStr(# the carrier of ((0). V), the U5 of ((0). V), the ZeroF of ((0). V), the lmult of ((0). V) #) is strict VectSpStr over F
(0). ((0). V) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (0). V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
A is Element of the carrier of W
T . A is Element of the carrier of V
A9 is Element of the carrier of W
T . A9 is Element of the carrier of V
A - A9 is Element of the carrier of W
- A9 is Element of the carrier of W
K176(W,A,(- A9)) is Element of the carrier of W
T . (A - A9) is Element of the carrier of V
(T . A) - (T . A9) is Element of the carrier of V
- (T . A9) is Element of the carrier of V
K176(V,(T . A),(- (T . A9))) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Element of K6( the carrier of V)
Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
T is Element of the carrier of V
A is Element of the carrier of V
T - A is Element of the carrier of V
- A is Element of the carrier of V
K176(V,T,(- A)) is Element of the carrier of V
{A} is non empty V2() finite 1 -element Element of K6( the carrier of V)
W \/ {A} is non empty Element of K6( the carrier of V)
Lin (W \/ {A}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
Lin {A} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
(Lin W) + (Lin {A}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
(T - A) + A is Element of the carrier of V
A - A is Element of the carrier of V
K176(V,A,(- A)) is Element of the carrier of V
T - (A - A) is Element of the carrier of V
- (A - A) is Element of the carrier of V
K176(V,T,(- (A - A))) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
T - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
K176(V,T,(- (0. V))) is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K6( the carrier of W) is non empty set
T is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
[#] W is non empty non proper Element of K6( the carrier of W)
A is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Element of K6( the carrier of V)
Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
[#] (Lin W) is non empty non proper Element of K6( the carrier of (Lin W))
the carrier of (Lin W) is non empty set
K6( the carrier of (Lin W)) is non empty set
T is set
A is Element of the carrier of V
T is Element of K6( the carrier of (Lin W))
Lin T is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of Lin W
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Element of K6( the carrier of V)
Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
T is Element of the carrier of V
{T} is non empty V2() finite 1 -element Element of K6( the carrier of V)
W \/ {T} is non empty Element of K6( the carrier of V)
[#] (Lin W) is non empty non proper Element of K6( the carrier of (Lin W))
the carrier of (Lin W) is non empty set
K6( the carrier of (Lin W)) is non empty set
A9 is Basis of Lin W
A is Element of K6( the carrier of (Lin W))
A9 \/ A is Element of K6( the carrier of (Lin W))
B is set
B is Element of K6( the carrier of (Lin W))
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
A is Element of K6( the carrier of W)
A9 is Basis of W
A9 \ A is Element of K6( the carrier of W)
T | (A9 \ A) is Relation-like the carrier of W -defined A9 \ A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))
X is set
dom (T | (A9 \ A)) is set
X is set
(T | (A9 \ A)) . X is set
(T | (A9 \ A)) . X is set
dom (T | (A9 \ A)) is Element of K6((A9 \ A))
K6((A9 \ A)) is non empty set
dom T is Element of K6( the carrier of W)
A is Element of the carrier of W
B is Element of K6( the carrier of W)
B is Element of the carrier of W
{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)
B \/ {B} is non empty Element of K6( the carrier of W)
(T | (A9 \ A)) . B is set
T . B is Element of the carrier of V
C is Basis of (F,W,V,T)
Lin C is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of (F,W,V,T)
(T | (A9 \ A)) . A is set
T . A is Element of the carrier of V
A - B is Element of the carrier of W
- B is Element of the carrier of W
K176(W,A,(- B)) is Element of the carrier of W
Lin B is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
Lin (B \/ {B}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
{A} is non empty V2() finite 1 -element Element of K6( the carrier of W)
{B} \/ {A} is non empty finite Element of K6( the carrier of W)
{A,B} is non empty finite Element of K6( the carrier of W)
(B \/ {B}) \/ {A} is non empty Element of K6( the carrier of W)
B \/ {A,B} is non empty Element of K6( the carrier of W)
C is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Element of K6( the carrier of V)
T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
A is Element of the carrier of V
{A} is non empty V2() finite 1 -element Element of K6( the carrier of V)
W \/ {A} is non empty Element of K6( the carrier of V)
A9 is Element of the carrier of F
T +* (A,A9) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
dom (T +* (A,A9)) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
rng (T +* (A,A9)) is set
[#] F is non empty non proper Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
B is set
X is set
(T +* (A,A9)) . X is set
dom T is Element of K6( the carrier of V)
T . X is set
rng T is set
Funcs (([#] V),([#] F)) is non empty FUNCTION_DOMAIN of [#] V, [#] F
Carrier T is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not T . b₁ = 0. F } is set
(Carrier T) \/ {A} is non empty finite Element of K6( the carrier of V)
B is Relation-like [#] V -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] V),([#] F))
X is Element of the carrier of V
B . X is set
T . X is Element of the carrier of F
X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier X is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0. F } is set
B is set
A is Element of the carrier of V
X . A is Element of the carrier of F
T . A is Element of the carrier of F
F is 1-sorted
the carrier of F is set
K6( the carrier of F) is non empty set
[#] F is non proper Element of K6( the carrier of F)
V is Element of K6( the carrier of F)
([#] F) \ V is Element of K6( the carrier of F)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
the carrier of F is non empty V2() set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
W .: T is set
K6( the carrier of F) is non empty set
(V,F,W,T) is Element of K6( the carrier of F)
[#] F is non empty non proper Element of K6( the carrier of F)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty V2() finite 1 -element Element of K6( the carrier of V)
W is Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
the carrier of F is non empty V2() set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,T) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ T is Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))
K7((V,T), the carrier of F) is Relation-like set
K6(K7((V,T), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,T),{(0. F)}) is Relation-like set
(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set
dom ((W | T) +* ((V,T) --> (0. F))) is set
dom (W | T) is Element of K6(T)
K6(T) is non empty set
dom ((V,T) --> (0. F)) is Element of K6((V,T))
K6((V,T)) is non empty set
(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set
dom W is Element of K6( the carrier of V)
T \/ (([#] V) \ T) is Element of K6( the carrier of V)
rng ((W | T) +* ((V,T) --> (0. F))) is set
[#] F is non empty non proper Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
A9 is set
B is set
((W | T) +* ((V,T) --> (0. F))) . B is set
B is Element of the carrier of V
((W | T) +* ((V,T) --> (0. F))) . B is set
(W | T) . B is set
W . B is Element of the carrier of F
B is Element of the carrier of V
((W | T) +* ((V,T) --> (0. F))) . B is set
((V,T) --> (0. F)) . B is set
B is Element of the carrier of V
Funcs (([#] V),([#] F)) is non empty FUNCTION_DOMAIN of [#] V, [#] F
A9 is Relation-like [#] V -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] V),([#] F))
{ b₁ where b₁ is Element of the carrier of V : not A9 . b₁ = 0. F } is set
B is set
X is Element of the carrier of V
A9 . X is set
Carrier W is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
B is Element of K6( the carrier of V)
X is set
B is Element of the carrier of V
A9 . B is set
((V,T) --> (0. F)) . B is set
(W | T) . B is set
W . B is Element of the carrier of F
X is finite Element of K6( the carrier of V)
B is Element of the carrier of V
A9 . B is set
B is finite Element of K6( the carrier of V)
B is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier B is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. F } is set
B is set
X is Element of the carrier of V
B . X is Element of the carrier of F
((V,T) --> (0. F)) . X is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier W is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
(F,V,W,(Carrier W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of Carrier W
W | (Carrier W) is Relation-like the carrier of V -defined Carrier W -defined the carrier of V -defined the carrier of F -valued Function-like finite Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,(Carrier W)) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ (Carrier W) is Element of K6( the carrier of V)
(V,(Carrier W)) --> (0. F) is Relation-like (V,(Carrier W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(Carrier W)), the carrier of F))
K7((V,(Carrier W)), the carrier of F) is Relation-like set
K6(K7((V,(Carrier W)), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,(Carrier W)),{(0. F)}) is Relation-like set
(W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F)) is Relation-like Function-like set
dom ((V,(Carrier W)) --> (0. F)) is Element of K6((V,(Carrier W)))
K6((V,(Carrier W))) is non empty set
dom W is Element of K6( the carrier of V)
dom (W | (Carrier W)) is finite Element of K6((Carrier W))
K6((Carrier W)) is non empty finite V38() set
(dom (W | (Carrier W))) \/ (dom ((V,(Carrier W)) --> (0. F))) is set
B is set
W . B is set
((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set
B is Element of the carrier of V
((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set
(W | (Carrier W)) . B is set
B is Element of the carrier of V
((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set
((V,(Carrier W)) --> (0. F)) . B is set
B is Element of the carrier of V
dom ((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
(F,V,W,T) is Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Carrier W is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
(F,V,W,(Carrier W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of Carrier W
W | (Carrier W) is Relation-like the carrier of V -defined Carrier W -defined the carrier of V -defined the carrier of F -valued Function-like finite Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,(Carrier W)) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ (Carrier W) is Element of K6( the carrier of V)
(V,(Carrier W)) --> (0. F) is Relation-like (V,(Carrier W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(Carrier W)), the carrier of F))
K7((V,(Carrier W)), the carrier of F) is Relation-like set
K6(K7((V,(Carrier W)), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,(Carrier W)),{(0. F)}) is Relation-like set
(W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F)) is Relation-like Function-like set
rng (W | (Carrier W)) is finite set
rng ((V,(Carrier W)) --> (0. F)) is V2() finite set
(rng (W | (Carrier W))) \/ (rng ((V,(Carrier W)) --> (0. F))) is finite set
rng W is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
(F,V,W,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T
W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,T) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ T is Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))
K7((V,T), the carrier of F) is Relation-like set
K6(K7((V,T), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,T),{(0. F)}) is Relation-like set
(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set
A is Element of the carrier of V
(F,V,W,T) . A is Element of the carrier of F
W . A is Element of the carrier of F
dom (F,V,W,T) is Element of K6( the carrier of V)
dom (W | T) is Element of K6(T)
K6(T) is non empty set
dom ((V,T) --> (0. F)) is Element of K6((V,T))
K6((V,T)) is non empty set
(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set
(W | T) . A is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
(F,V,W,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T
W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,T) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ T is Element of K6( the carrier of V)
(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))
K7((V,T), the carrier of F) is Relation-like set
K6(K7((V,T), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,T),{(0. F)}) is Relation-like set
(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set
A is Element of the carrier of V
(F,V,W,T) . A is Element of the carrier of F
dom (F,V,W,T) is Element of K6( the carrier of V)
dom ((V,T) --> (0. F)) is Element of K6((V,T))
K6((V,T)) is non empty set
dom (W | T) is Element of K6(T)
K6(T) is non empty set
(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set
((V,T) --> (0. F)) . A is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
T is Element of K6( the carrier of V)
W is Element of K6( the carrier of V)
T \ W is Element of K6( the carrier of V)
A is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T
(F,V,A,W) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
A | W is Relation-like the carrier of V -defined W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,W) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ W is Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(V,W) --> (0. F) is Relation-like (V,W) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,W), the carrier of F))
K7((V,W), the carrier of F) is Relation-like set
K6(K7((V,W), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,W),{(0. F)}) is Relation-like set
(A | W) +* ((V,W) --> (0. F)) is Relation-like Function-like set
(F,V,A,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T \ W
A | (T \ W) is Relation-like the carrier of V -defined T \ W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
(V,(T \ W)) is Element of K6( the carrier of V)
([#] V) \ (T \ W) is Element of K6( the carrier of V)
(V,(T \ W)) --> (0. F) is Relation-like (V,(T \ W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(T \ W)), the carrier of F))
K7((V,(T \ W)), the carrier of F) is Relation-like set
K6(K7((V,(T \ W)), the carrier of F)) is non empty set
K7((V,(T \ W)),{(0. F)}) is Relation-like set
(A | (T \ W)) +* ((V,(T \ W)) --> (0. F)) is Relation-like Function-like set
(F,V,A,W) + (F,V,A,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
B is Element of the carrier of V
A . B is set
((F,V,A,W) + (F,V,A,(T \ W))) . B is set
W \/ (T \ W) is Element of K6( the carrier of V)
(F,V,A,(T \ W)) . B is Element of the carrier of F
(F,V,A,W) . B is Element of the carrier of F
A . B is Element of the carrier of F
((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F
(A . B) + (0. F) is Element of the carrier of F
(F,V,A,W) . B is Element of the carrier of F
(F,V,A,(T \ W)) . B is Element of the carrier of F
A . B is Element of the carrier of F
((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F
(0. F) + (A . B) is Element of the carrier of F
Carrier A is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. F } is set
(F,V,A,(T \ W)) . B is Element of the carrier of F
(F,V,A,W) . B is Element of the carrier of F
((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F
(0. F) + (0. F) is Element of the carrier of F
A . B is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
the carrier of F is non empty V2() set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
T is Element of K6( the carrier of V)
(F,V,W,T) is Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
F is non empty 1-sorted
the carrier of F is non empty set
V is non empty 1-sorted
the carrier of V is non empty set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of F, the carrier of V)) is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))
T is Element of K6( the carrier of V)
W " T is set
K6( the carrier of F) is non empty set
dom W is Element of K6( the carrier of F)
[#] F is non empty non proper Element of K6( the carrier of F)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier W is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
T is Element of K6( the carrier of V)
(F,V,W,T) is finite Element of K6( the carrier of F)
A9 is set
dom W is Element of K6( the carrier of V)
B is set
W . B is set
B is Element of the carrier of V
W . B is Element of the carrier of F
(Carrier W) /\ T is finite Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
the carrier of F is non empty V2() set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
A is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
[#] W is non empty non proper Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
A9 is set
B is Element of the carrier of W
{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{B}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F
A9 is Relation-like Function-like set
dom A9 is set
rng A9 is set
[#] F is non empty non proper Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
B is set
B is set
A9 . B is set
X is Element of the carrier of W
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{X}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F
B is Element of the carrier of W
A9 . B is set
{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{B}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F
B is Element of the carrier of W
{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{B}) is Element of K6( the carrier of V)
(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F
Funcs (([#] W),([#] F)) is non empty FUNCTION_DOMAIN of [#] W, [#] F
B is Relation-like [#] W -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] W),([#] F))
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not B . b₁ = 0. F } is set
X is set
X is Element of the carrier of W
B . X is set
Carrier T is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not T . b₁ = 0. F } is set
(V,W,A,(Carrier T)) is finite Element of K6( the carrier of W)
X is Element of K6( the carrier of W)
B is Element of K6( the carrier of W)
A is set
C is Element of the carrier of W
B . C is set
{C} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{C}) is Element of K6( the carrier of V)
(F,V,T,(V,W,A,{C})) is finite Element of K6( the carrier of F)
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{C})) is Element of the carrier of F
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
C is set
L is set
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
C is set
dom A is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
L is Element of the carrier of V
A . L is Element of the carrier of W
A is finite Element of K6( the carrier of W)
C is Element of the carrier of W
B . C is set
X is finite Element of K6( the carrier of W)
B is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
X is Element of the carrier of W
B . X is Element of the carrier of F
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{X}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F
X is Element of the carrier of W
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{X}) is Element of K6( the carrier of V)
(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F
X is Element of the carrier of W
B . X is Element of the carrier of F
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{X}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)
Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F
A9 is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
B is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
dom A9 is Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
B is set
A9 . B is set
B . B is set
X is Element of the carrier of W
A9 . X is Element of the carrier of F
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,A,{X}) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F
[#] W is non empty non proper Element of K6( the carrier of W)
dom B is Element of K6( the carrier of W)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier A is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not A . b₁ = 0. F } is set
(W,V,T,(Carrier A)) is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
Carrier (F,W,V,A,T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (F,W,V,A,T) . b₁ = 0. F } is set
A9 is set
B is Element of the carrier of V
(F,W,V,A,T) . B is Element of the carrier of F
{B} is non empty V2() finite 1 -element Element of K6( the carrier of V)
(W,V,T,{B}) is Element of K6( the carrier of W)
(F,W,A,(W,V,T,{B})) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
Sum (F,W,A,(W,V,T,{B})) is Element of the carrier of F
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
B is set
X is set
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
B is set
dom T is Element of K6( the carrier of W)
T . B is set
X is Element of the carrier of W
T . X is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier (F,W,V,A,T) is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not (F,W,V,A,T) . b₁ = 0. F } is set
Carrier A is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
{ b₁ where b₁ is Element of the carrier of W : not A . b₁ = 0. F } is set
(W,V,T,(Carrier A)) is finite Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier W is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier T is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not T . b₁ = 0. F } is set
W + T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier (W + T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (W + T) . b₁ = 0. F } is set
(Carrier W) \/ (Carrier T) is finite Element of K6( the carrier of V)
A is set
A9 is Element of the carrier of V
(W + T) . A9 is Element of the carrier of F
W . A9 is Element of the carrier of F
T . A9 is Element of the carrier of F
(W . A9) + (T . A9) is Element of the carrier of F
A9 is Element of the carrier of V
(W + T) . A9 is Element of the carrier of F
W . A9 is Element of the carrier of F
T . A9 is Element of the carrier of F
(W . A9) + (T . A9) is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier W is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier T is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not T . b₁ = 0. F } is set
W - T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
- T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1. F) is Element of the carrier of F
(- (1. F)) * T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
W + (- T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier (W - T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (W - T) . b₁ = 0. F } is set
(Carrier W) \/ (Carrier T) is finite Element of K6( the carrier of V)
Carrier (- T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (- T) . b₁ = 0. F } is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Element of K6( the carrier of V)
T is Element of K6( the carrier of V)
Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
T \ W is Element of K6( the carrier of V)
Lin (T \ W) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
(Lin W) /\ (Lin (T \ W)) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
the carrier of ((Lin W) /\ (Lin (T \ W))) is non empty set
A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of (Lin W) /\ (Lin (T \ W))
B is Element of the carrier of ((Lin W) /\ (Lin (T \ W)))
the carrier of F is non empty V2() set
B is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Sum B is Element of the carrier of V
X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T \ W
Sum X is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
(Sum B) - (Sum X) is Element of the carrier of V
- (Sum X) is Element of the carrier of V
K176(V,(Sum B),(- (Sum X))) is Element of the carrier of V
B - X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
- X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1. F) is Element of the carrier of F
(- (1. F)) * X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
B + (- X) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Sum (B - X) is Element of the carrier of V
Carrier (B - X) is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not (B - X) . b₁ = 0. F } is set
Carrier B is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. F } is set
Carrier X is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0. F } is set
(Carrier B) \/ (Carrier X) is finite Element of K6( the carrier of V)
W \/ (T \ W) is Element of K6( the carrier of V)
X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T
Carrier X is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0. F } is set
ZeroLC V is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
(Omega). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
the U5 of V is Relation-like K7( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of V, the carrier of V), the carrier of V))
K7( the carrier of V, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of V, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( 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 K7( the carrier of F, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of V), the carrier of V))
the carrier of F is non empty V2() set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of F, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( the carrier of F, the carrier of V), the carrier of V)) is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is strict VectSpStr over F
(Lin W) + (Lin (T \ W)) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
[#] V is non empty non proper Element of K6( the carrier of V)
[#] ((Lin W) + (Lin (T \ W))) is non empty non proper Element of K6( the carrier of ((Lin W) + (Lin (T \ W))))
the carrier of ((Lin W) + (Lin (T \ W))) is non empty set
K6( the carrier of ((Lin W) + (Lin (T \ W)))) is non empty set
A9 is set
Lin T is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V
B is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T
Sum B is Element of the carrier of V
(F,V,B,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T \ W
B | (T \ W) is Relation-like the carrier of V -defined T \ W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,(T \ W)) is Element of K6( the carrier of V)
([#] V) \ (T \ W) is Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(V,(T \ W)) --> (0. F) is Relation-like (V,(T \ W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(T \ W)), the carrier of F))
K7((V,(T \ W)), the carrier of F) is Relation-like set
K6(K7((V,(T \ W)), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,(T \ W)),{(0. F)}) is Relation-like set
(B | (T \ W)) +* ((V,(T \ W)) --> (0. F)) is Relation-like Function-like set
(F,V,B,W) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
B | W is Relation-like the carrier of V -defined W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
(V,W) is Element of K6( the carrier of V)
([#] V) \ W is Element of K6( the carrier of V)
(V,W) --> (0. F) is Relation-like (V,W) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,W), the carrier of F))
K7((V,W), the carrier of F) is Relation-like set
K6(K7((V,W), the carrier of F)) is non empty set
K7((V,W),{(0. F)}) is Relation-like set
(B | W) +* ((V,W) --> (0. F)) is Relation-like Function-like set
(F,V,B,W) + (F,V,B,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Sum (F,V,B,W) is Element of the carrier of V
Sum (F,V,B,(T \ W)) is Element of the carrier of V
(Sum (F,V,B,W)) + (Sum (F,V,B,(T \ W))) is Element of the carrier of V
B is Element of the carrier of V
A is Element of the carrier of V
B + A is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Element of K6( the carrier of W)
T | A is Relation-like the carrier of W -defined A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))
B is Element of the carrier of W
T . B is Element of the carrier of V
{(T . B)} is non empty V2() finite 1 -element Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(W,V,T,{(T . B)}) is Element of K6( the carrier of W)
{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(W,V,T,{(T . B)}) \ {B} is Element of K6( the carrier of W)
dom T is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
dom (T | A) is Element of K6(A)
K6(A) is non empty set
X is set
T . X is set
(T | A) . X is set
(T | A) . B is set
{B} \/ ((W,V,T,{(T . B)}) \ {B}) is non empty Element of K6( the carrier of W)
X is set
dom T is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier W is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not W . b₁ = 0. F } is set
T is Element of K6( the carrier of V)
(F,V,W,T) is finite Element of K6( the carrier of F)
dom W is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
A is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
(F,V,W,A,T) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Carrier (F,V,W,A,T) is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not (F,V,W,A,T) . b₁ = 0. F } is set
Carrier A is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. F } is set
A9 is Element of the carrier of W
{A9} is non empty V2() finite 1 -element Element of K6( the carrier of W)
(V,W,T,{A9}) is Element of K6( the carrier of V)
(F,V,W,A,T) . A9 is Element of the carrier of F
(F,V,A,(V,W,T,{A9})) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Sum (F,V,A,(V,W,T,{A9})) is Element of the carrier of F
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
Sum ({} F) is Element of the carrier of F
(F,V,A,(V,W,T,{A9})) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
Sum (F,V,A,(V,W,T,{A9})) is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Carrier A is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not A . b₁ = 0. F } is set
T | (Carrier A) is Relation-like the carrier of W -defined Carrier A -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
A9 is Element of the carrier of W
T . A9 is Element of the carrier of V
(F,W,V,A,T) . (T . A9) is Element of the carrier of F
A . A9 is Element of the carrier of F
{(T . A9)} is non empty V2() finite 1 -element Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(W,V,T,{(T . A9)}) is Element of K6( the carrier of W)
{A9} is non empty V2() finite 1 -element Element of K6( the carrier of W)
B is Element of K6( the carrier of W)
{A9} \/ B is non empty Element of K6( the carrier of W)
dom A is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
(F,W,A,{A9}) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Im (A,A9) is set
{A9} is non empty V2() finite 1 -element set
A .: {A9} is finite set
{(A . A9)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
(F,W,A,(W,V,T,{(T . A9)})) is finite Element of K6( the carrier of F)
Sum (F,W,A,(W,V,T,{(T . A9)})) is Element of the carrier of F
(F,W,A,B) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
B is set
dom A is Element of K6( the carrier of W)
X is set
A . X is set
(Carrier A) /\ B is finite Element of K6( the carrier of W)
X is Element of the carrier of W
A . X is Element of the carrier of F
(F,W,A,{A9}) is finite Element of K6( the carrier of F)
B is set
dom A is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
Im (A,A9) is set
{A9} is non empty V2() finite 1 -element set
A .: {A9} is finite set
{(A . A9)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
dom A is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
B is set
(Carrier A) /\ B is finite Element of K6( the carrier of W)
X is set
X is Element of the carrier of W
A . X is Element of the carrier of F
Im (A,A9) is set
{A9} is non empty V2() finite 1 -element set
A .: {A9} is finite set
{(A . A9)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
(F,W,A,(W,V,T,{(T . A9)})) is finite Element of K6( the carrier of F)
(F,W,A,{A9}) \/ (F,W,A,B) is finite Element of K6( the carrier of F)
Sum (F,W,A,(W,V,T,{(T . A9)})) is Element of the carrier of F
Sum (F,W,A,{A9}) is Element of the carrier of F
Sum (F,W,A,B) is Element of the carrier of F
(Sum (F,W,A,{A9})) + (Sum (F,W,A,B)) is Element of the carrier of F
Sum {(0. F)} is Element of the carrier of F
(A . A9) + (Sum {(0. F)}) is Element of the carrier of F
(A . A9) + (0. F) is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Carrier A is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not A . b₁ = 0. F } is set
T | (Carrier A) is Relation-like the carrier of W -defined Carrier A -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
A9 is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
rng A9 is finite set
A (#) A9 is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
T * (A (#) A9) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
T * A9 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(F,W,V,A,T) (#) (T * A9) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
len (T * A9) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
len A9 is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
len (A (#) A9) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
dom B is finite Element of K6(NAT)
Seg (len A9) is finite len A9 -element Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT : ( 1 <= b₁ & b₁ <= len A9 ) } is set
X is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
B . X is set
B . X is set
A9 /. X is Element of the carrier of W
dom (A (#) A9) is finite Element of K6(NAT)
dom A9 is finite Element of K6(NAT)
A9 . X is set
(T * A9) . X is set
B is Element of the carrier of W
T . B is Element of the carrier of V
(A (#) A9) . X is set
X is Element of the carrier of W
A . X is Element of the carrier of F
(A . X) * X is Element of the carrier of W
T . ((A . X) * X) is Element of the carrier of V
T . X is Element of the carrier of V
(A . X) * (T . X) is Element of the carrier of V
A . B is Element of the carrier of F
A is Element of the carrier of V
(A . B) * A is Element of the carrier of V
T . (A9 . X) is set
(F,W,V,A,T) . ((T * A9) . X) is set
A . (A9 . X) is set
dom T is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
dom (T * A9) is finite Element of K6(NAT)
(T * A9) /. X is Element of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Carrier A is finite Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not A . b₁ = 0. F } is set
T | (Carrier A) is Relation-like the carrier of W -defined Carrier A -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
(W,V,T,(Carrier A)) is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier (F,W,V,A,T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (F,W,V,A,T) . b₁ = 0. F } is set
A9 is set
dom T is Element of K6( the carrier of W)
B is set
T . B is set
B is Element of the carrier of W
T . B is Element of the carrier of V
(F,W,V,A,T) . (T . B) is Element of the carrier of F
A . B is Element of the carrier of F
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W
A is Element of K6( the carrier of W)
A9 is Basis of W
A9 \ A is Element of K6( the carrier of W)
B is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of A9 \ A
Sum B is Element of the carrier of W
T . (Sum B) is Element of the carrier of V
(F,W,V,B,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Sum (F,W,V,B,T) is Element of the carrier of V
T | (A9 \ A) is Relation-like the carrier of W -defined A9 \ A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))
Carrier B is finite Element of K6( the carrier of W)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not B . b₁ = 0. F } is set
(T | (A9 \ A)) | (Carrier B) is Relation-like the carrier of W -defined Carrier B -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
T | (Carrier B) is Relation-like the carrier of W -defined Carrier B -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
B is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
rng B is finite set
B (#) B is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
Sum (B (#) B) is Element of the carrier of W
T * B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
X is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng X is finite set
(W,V,T,(Carrier B)) is finite Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
Carrier (F,W,V,B,T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (F,W,V,B,T) . b₁ = 0. F } is set
dom T is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
(F,W,V,B,T) (#) X is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((F,W,V,B,T) (#) X) is Element of the carrier of V
T * (B (#) B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
W is Element of K6( the carrier of V)
T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Sum T is Element of the carrier of V
Carrier T is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not T . b₁ = 0. F } is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
K6( the carrier of V) is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
the carrier of F is non empty V2() set
A is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
T is Element of K6( the carrier of V)
(V,W,A,T) is Element of K6( the carrier of W)
K6( the carrier of W) is non empty set
A | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of W -valued Function-like Element of K6(K7( the carrier of V, the carrier of W))
A9 is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of (V,W,A,T)
A9 * A is Relation-like the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))
K7( the carrier of V, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of F)) is non empty set
(V,T) is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
([#] V) \ T is Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))
K7((V,T), the carrier of F) is Relation-like set
K6(K7((V,T), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((V,T),{(0. F)}) is Relation-like set
(A9 * A) +* ((V,T) --> (0. F)) is Relation-like Function-like set
rng (A9 * A) is set
rng A9 is set
[#] F is non empty non proper Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
dom A9 is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
rng A is set
dom (A9 * A) is Element of K6( the carrier of V)
dom A is Element of K6( the carrier of V)
dom ((V,T) --> (0. F)) is Element of K6((V,T))
K6((V,T)) is non empty set
rng ((V,T) --> (0. F)) is V2() finite set
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
rng ((A9 * A) +* ((V,T) --> (0. F))) is set
(rng (A9 * A)) \/ (rng ((V,T) --> (0. F))) is set
([#] V) \/ (([#] V) \ T) is non empty Element of K6( the carrier of V)
dom ((A9 * A) +* ((V,T) --> (0. F))) is set
Funcs (([#] V),([#] F)) is non empty FUNCTION_DOMAIN of [#] V, [#] F
B is Relation-like [#] V -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] V),([#] F))
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. F } is set
X is set
B is Element of the carrier of V
B . B is set
X is Element of K6( the carrier of V)
Carrier A9 is finite Element of K6( the carrier of W)
{ b₁ where b₁ is Element of the carrier of W : not A9 . b₁ = 0. F } is set
(V,W,A,(Carrier A9)) is Element of K6( the carrier of V)
(V,W,A,(Carrier A9)) /\ T is Element of K6( the carrier of V)
A | ((V,W,A,(Carrier A9)) /\ T) is Relation-like the carrier of V -defined (V,W,A,(Carrier A9)) /\ T -defined the carrier of V -defined the carrier of W -valued Function-like Element of K6(K7( the carrier of V, the carrier of W))
dom (A | ((V,W,A,(Carrier A9)) /\ T)) is set
rng (A | ((V,W,A,(Carrier A9)) /\ T)) is set
C is set
C is Element of the carrier of V
B . C is set
((V,T) --> (0. F)) . C is set
L is Element of the carrier of V
B . L is set
(A9 * A) . C is set
A . C is Element of the carrier of W
A9 . (A . C) is Element of the carrier of F
L is Element of the carrier of V
B . L is set
C is set
dom (A | ((V,W,A,(Carrier A9)) /\ T)) is Element of K6(((V,W,A,(Carrier A9)) /\ T))
K6(((V,W,A,(Carrier A9)) /\ T)) is non empty set
C is set
(A | ((V,W,A,(Carrier A9)) /\ T)) . C is set
A . C is set
C is set
A . C is set
C is Element of the carrier of V
A . C is Element of the carrier of W
A9 . (A . C) is Element of the carrier of F
B . C is set
(A9 * A) . C is set
card X is V4() V5() V6() cardinal set
card (Carrier A9) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
B is Relation-like Function-like set
dom B is set
rng B is set
B is finite Element of K6( the carrier of V)
A is Element of the carrier of V
B . A is set
X is finite Element of K6( the carrier of V)
X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier X is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0. F } is set
X is set
B is Element of the carrier of V
X . B is Element of the carrier of F
((V,T) --> (0. F)) . B is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Element of K6( the carrier of W)
(W,V,T,A) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
T | A is Relation-like the carrier of W -defined A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))
A9 is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of (W,V,T,A)
(F,W,V,A,T,A9) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of A
B is Element of the carrier of W
(F,W,V,A,T,A9) . B is Element of the carrier of F
T . B is Element of the carrier of V
A9 . (T . B) is Element of the carrier of F
(W,A) is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
([#] W) \ A is Element of K6( the carrier of W)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(W,A) --> (0. F) is Relation-like (W,A) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((W,A), the carrier of F))
K7((W,A), the carrier of F) is Relation-like set
K6(K7((W,A), the carrier of F)) is non empty set
{(0. F)} is non empty V2() finite 1 -element set
K7((W,A),{(0. F)}) is Relation-like set
dom ((W,A) --> (0. F)) is Element of K6((W,A))
K6((W,A)) is non empty set
A9 * T is Relation-like the carrier of W -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of W, the carrier of F))
K7( the carrier of W, the carrier of F) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of F)) is non empty set
(A9 * T) +* ((W,A) --> (0. F)) is Relation-like Function-like set
(A9 * T) . B is set
dom T is Element of K6( the carrier of W)
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
the carrier of F is non empty V2() set
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F
the carrier of W is non empty set
K7( the carrier of W, the carrier of V) is non empty Relation-like set
K6(K7( the carrier of W, the carrier of V)) is non empty set
K6( the carrier of W) is non empty set
T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))
A is Element of K6( the carrier of W)
(W,V,T,A) is Element of K6( the carrier of V)
K6( the carrier of V) is non empty set
T | A is Relation-like the carrier of W -defined A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))
A9 is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of (W,V,T,A)
(F,W,V,A,T,A9) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of A
(F,W,V,(F,W,V,A,T,A9),T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
B is Element of the carrier of V
(F,W,V,(F,W,V,A,T,A9),T) . B is set
A9 . B is set
Carrier A9 is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not A9 . b₁ = 0. F } is set
A9 . B is Element of the carrier of F
dom (F,W,V,A,T,A9) is Element of K6( the carrier of W)
[#] W is non empty non proper Element of K6( the carrier of W)
dom T is Element of K6( the carrier of W)
X is set
T . X is set
X is Element of the carrier of W
T . X is Element of the carrier of V
{(T . X)} is non empty V2() finite 1 -element Element of K6( the carrier of V)
(W,V,T,{(T . X)}) is Element of K6( the carrier of W)
{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)
B is Element of K6( the carrier of W)
{X} \/ B is non empty Element of K6( the carrier of W)
(F,W,V,A,T,A9) . X is Element of the carrier of F
A9 . (T . X) is Element of the carrier of F
(F,W,(F,W,V,A,T,A9),{X}) is finite Element of K6( the carrier of F)
K6( the carrier of F) is non empty set
Im ((F,W,V,A,T,A9),X) is set
{X} is non empty V2() finite 1 -element set
(F,W,V,A,T,A9) .: {X} is finite set
{((F,W,V,A,T,A9) . X)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
(F,W,V,(F,W,V,A,T,A9),T) . B is Element of the carrier of F
(F,W,(F,W,V,A,T,A9),(W,V,T,{(T . X)})) is finite Element of K6( the carrier of F)
Sum (F,W,(F,W,V,A,T,A9),(W,V,T,{(T . X)})) is Element of the carrier of F
{(A9 . (T . X))} is non empty V2() finite 1 -element Element of K6( the carrier of F)
(F,W,(F,W,V,A,T,A9),B) is finite Element of K6( the carrier of F)
{(A9 . (T . X))} \/ (F,W,(F,W,V,A,T,A9),B) is non empty finite Element of K6( the carrier of F)
Sum ({(A9 . (T . X))} \/ (F,W,(F,W,V,A,T,A9),B)) is Element of the carrier of F
{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)
{(A9 . (T . X))} \/ ({} F) is non empty finite Element of K6( the carrier of F)
Sum ({(A9 . (T . X))} \/ ({} F)) is Element of the carrier of F
Carrier (F,W,V,A,T,A9) is finite Element of K6( the carrier of W)
{ b₁ where b₁ is Element of the carrier of W : not (F,W,V,A,T,A9) . b₁ = 0. F } is set
{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)
{(A9 . (T . X))} \/ {(0. F)} is non empty finite Element of K6( the carrier of F)
Sum ({(A9 . (T . X))} \/ {(0. F)}) is Element of the carrier of F
Sum {(A9 . (T . X))} is Element of the carrier of F
Sum {(0. F)} is Element of the carrier of F
(Sum {(A9 . (T . X))}) + (Sum {(0. F)}) is Element of the carrier of F
(A9 . (T . X)) + (Sum {(0. F)}) is Element of the carrier of F
(A9 . (T . X)) + (0. F) is Element of the carrier of F
Carrier A9 is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not A9 . b₁ = 0. F } is set
A9 . B is Element of the carrier of F
(F,W,V,(F,W,V,A,T,A9),T) . B is Element of the carrier of F
Carrier (F,W,V,(F,W,V,A,T,A9),T) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (F,W,V,(F,W,V,A,T,A9),T) . b₁ = 0. F } is set
{B} is non empty V2() finite 1 -element Element of K6( the carrier of V)
(W,V,T,{B}) is Element of K6( the carrier of W)
Carrier (F,W,V,A,T,A9) is finite Element of K6( the carrier of W)
{ b₁ where b₁ is Element of the carrier of W : not (F,W,V,A,T,A9) . b₁ = 0. F } is set
X is Element of the carrier of W
T . X is Element of the carrier of V
T | (Carrier (F,W,V,A,T,A9)) is Relation-like the carrier of W -defined Carrier (F,W,V,A,T,A9) -defined the carrier of W -defined the carrier of V -valued Function-like finite Element of K6(K7( the carrier of W, the carrier of V))
(F,W,V,A,T,A9) . X is Element of the carrier of F
Carrier A9 is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not A9 . b₁ = 0. F } is set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of W
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
(F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of W
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) + (F,V,W,T) is V11() ext-real V46() set
the finite Basis of (F,V,W,T) is finite Basis of (F,V,W,T)
K6( the carrier of V) is non empty set
B is Basis of V
B is finite Element of K6( the carrier of V)
K6(B) is non empty finite V38() set
A9 is Element of K6( the carrier of V)
B \ A9 is finite Element of K6( the carrier of V)
X is finite Element of K6(B)
X is finite Element of K6( the carrier of V)
the finite Basis of (F,V,W,T) \/ X is finite set
K6( the carrier of W) is non empty set
(V,W,T,X) is finite Element of K6( the carrier of W)
T | X is Relation-like the carrier of V -defined X -defined the carrier of V -defined the carrier of W -valued Function-like finite Element of K6(K7( the carrier of V, the carrier of W))
C is finite Element of K6( the carrier of W)
the carrier of F is non empty V2() set
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
C is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of C
Carrier C is finite Element of K6( the carrier of W)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of W : not C . b₁ = 0. F } is set
Sum C is Element of the carrier of W
L is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of (V,W,T,X)
(F,V,W,X,T,L) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of X
(F,V,W,(F,V,W,X,T,L),T) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
B is finite Basis of V
B \ A9 is finite Element of K6( the carrier of V)
L is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of X
(F,V,W,L,T) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
L is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of B \ A9
(F,V,W,L,T) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Sum L is Element of the carrier of V
T . (Sum L) is Element of the carrier of W
A is finite Basis of (F,V,W,T)
Lin A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (F,V,W,T)
Lin A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
C is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of A9
Sum C is Element of the carrier of V
L - C is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
- C is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
1. F is V55(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1. F) is Element of the carrier of F
(- (1. F)) * C is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
L + (- C) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V
Carrier (L - C) is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (L - C) . b₁ = 0. F } is set
Carrier L is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not L . b₁ = 0. F } is set
Carrier C is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not C . b₁ = 0. F } is set
(Carrier L) \/ (Carrier C) is finite Element of K6( the carrier of V)
(B \ A9) \/ A9 is Element of K6( the carrier of V)
(B \ A9) \/ A is finite set
(Sum L) - (Sum C) is Element of the carrier of V
- (Sum C) is Element of the carrier of V
K176(V,(Sum L),(- (Sum C))) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
Sum (L - C) is Element of the carrier of V
C is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of B
Carrier C is finite Element of K6( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not C . b₁ = 0. F } is set
(V,W,T,(Carrier L)) is finite Element of K6( the carrier of W)
dom T is Element of K6( the carrier of V)
[#] V is non empty non proper Element of K6( the carrier of V)
dom (T | X) is finite Element of K6(X)
K6(X) is non empty finite V38() set
(T | X) .: X is finite set
card C is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
card X is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
the carrier of (F,V,W,T) is non empty set
K6( the carrier of (F,V,W,T)) is non empty set
C is finite Element of K6( the carrier of (F,V,W,T))
Lin C is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (F,V,W,T)
L is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (F,V,W,T)
A is finite Basis of (F,V,W,T)
C is Element of the carrier of (F,V,W,T)
v9 is Element of the carrier of W
u is Element of the carrier of V
T . u is Element of the carrier of W
C is Element of K6( the carrier of V)
Lin C is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
B is finite Basis of V
B \ C is finite Element of K6( the carrier of V)
Lin (B \ C) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
(Omega). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
the U5 of V is Relation-like K7( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of V, the carrier of V), the carrier of V))
K7( the carrier of V, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of V, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( 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 K7( the carrier of F, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of V), the carrier of V))
the carrier of F is non empty V2() set
K7( the carrier of F, the carrier of V) is non empty Relation-like set
K7(K7( the carrier of F, the carrier of V), the carrier of V) is non empty Relation-like set
K6(K7(K7( the carrier of F, the carrier of V), the carrier of V)) is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is strict VectSpStr over F
(Lin C) + (Lin (B \ C)) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
u1 is Element of the carrier of V
u2 is Element of the carrier of V
u1 + u2 is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of B \ C
Sum l is Element of the carrier of V
Lin A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (F,V,W,T)
T . u1 is Element of the carrier of W
0. W is V55(W) Element of the carrier of W
the ZeroF of W is Element of the carrier of W
(F,V,W,l,T) is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W
Carrier l is finite Element of K6( the carrier of V)
0. F is V55(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. F } is set
(V,W,T,(Carrier l)) is finite Element of K6( the carrier of W)
C9 is Element of K6( the carrier of W)
T . u2 is Element of the carrier of W
(T . u1) + (T . u2) is Element of the carrier of W
m is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of C9
Sum m is Element of the carrier of W
Lin C9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of W
c₂₅ is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of C9
Sum c₂₅ is Element of the carrier of W
C is linearly-independent Element of K6( the carrier of (F,V,W,T))
A is finite Basis of (F,V,W,T)
card A is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
C is finite Basis of (F,V,W,T)
card C is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
B is finite Basis of V
card B is V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT
F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()
V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of V is non empty set
W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F
the carrier of W is non empty set
K7( the carrier of V, the carrier of W) is non empty Relation-like set
K6(K7( the carrier of V, the carrier of W)) is non empty set
dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))
(F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of W
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V
(F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
dim (F,V,W,T) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set
(F,V,W,T) + (F,V,W,T) is V11() ext-real V46() set