:: 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