:: PENCIL_4 semantic presentation

REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is set
RAT is set
INT is set
{} is set
the empty V21() V22() V23() V25() V26() V27() finite V32() cardinal {} -element V51() ext-real non positive non negative V125() set is empty V21() V22() V23() V25() V26() V27() finite V32() cardinal {} -element V51() ext-real non positive non negative V125() set
2 is non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() Element of NAT
1 is non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() Element of NAT
K430() is set
{{}} is non empty trivial finite 1 -element set
K227({{}}) is M15({{}})
[:K227({{}}),{{}}:] is set
bool [:K227({{}}),{{}}:] is non empty set
K36(K227({{}}),{{}}) is set
card {} is V21() V22() V23() cardinal set
0 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
3 is non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() Element of NAT
K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
3 - 1 is V51() ext-real V125() set
(S + 1) - 1 is V51() ext-real V125() set
K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is finite set
card S is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
bool S is non empty finite V32() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
the carrier of K is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
the carrier of L is non empty set
the carrier of ((Omega). K) is non empty set
0. L is V44(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
0. ((Omega). K) is V44( (Omega). K) Element of the carrier of ((Omega). K)
the ZeroF of ((Omega). K) is Element of the carrier of ((Omega). K)
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the U5 of ((Omega). K) is V6() V18([: the carrier of ((Omega). K), the carrier of ((Omega). K):], the carrier of ((Omega). K)) Element of bool [:[: the carrier of ((Omega). K), the carrier of ((Omega). K):], the carrier of ((Omega). K):]
[: the carrier of ((Omega). K), the carrier of ((Omega). K):] is non empty set
[:[: the carrier of ((Omega). K), the carrier of ((Omega). K):], the carrier of ((Omega). K):] is non empty set
bool [:[: the carrier of ((Omega). K), the carrier of ((Omega). K):], the carrier of ((Omega). K):] is non empty set
K109( the U5 of ((Omega). K), the carrier of L) is set
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
the lmult of ((Omega). K) is V6() V18([: the carrier of S, the carrier of ((Omega). K):], the carrier of ((Omega). K)) Element of bool [:[: the carrier of S, the carrier of ((Omega). K):], the carrier of ((Omega). K):]
[: the carrier of S, the carrier of ((Omega). K):] is non empty set
[:[: the carrier of S, the carrier of ((Omega). K):], the carrier of ((Omega). K):] is non empty set
bool [:[: the carrier of S, the carrier of ((Omega). K):], the carrier of ((Omega). K):] is non empty set
K5( the lmult of ((Omega). K),[: the carrier of S, the carrier of L:]) is V1() set
0. K is V44(K) Element of the carrier of K
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
the carrier of K is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of (Omega). K
the carrier of L is non empty set
0. L is V44(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
0. K is V44(K) Element of the carrier of K
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
K109( the U5 of K, the carrier of L) is set
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
K5( the lmult of K,[: the carrier of S, the carrier of L:]) is V1() set
0. ((Omega). K) is V44( (Omega). K) Element of the carrier of ((Omega). K)
the carrier of ((Omega). K) is non empty set
the ZeroF of ((Omega). K) is Element of the carrier of ((Omega). K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
the carrier of ((Omega). L) is non empty set
the carrier of K is non empty set
0. ((Omega). L) is V44( (Omega). L) Element of the carrier of ((Omega). L)
the ZeroF of ((Omega). L) is Element of the carrier of ((Omega). L)
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the U5 of ((Omega). L) is V6() V18([: the carrier of ((Omega). L), the carrier of ((Omega). L):], the carrier of ((Omega). L)) Element of bool [:[: the carrier of ((Omega). L), the carrier of ((Omega). L):], the carrier of ((Omega). L):]
[: the carrier of ((Omega). L), the carrier of ((Omega). L):] is non empty set
[:[: the carrier of ((Omega). L), the carrier of ((Omega). L):], the carrier of ((Omega). L):] is non empty set
bool [:[: the carrier of ((Omega). L), the carrier of ((Omega). L):], the carrier of ((Omega). L):] is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
K109( the U5 of K, the carrier of ((Omega). L)) is set
the lmult of ((Omega). L) is V6() V18([: the carrier of S, the carrier of ((Omega). L):], the carrier of ((Omega). L)) Element of bool [:[: the carrier of S, the carrier of ((Omega). L):], the carrier of ((Omega). L):]
[: the carrier of S, the carrier of ((Omega). L):] is non empty set
[:[: the carrier of S, the carrier of ((Omega). L):], the carrier of ((Omega). L):] is non empty set
bool [:[: the carrier of S, the carrier of ((Omega). L):], the carrier of ((Omega). L):] is non empty set
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
K5( the lmult of K,[: the carrier of S, the carrier of ((Omega). L):]) is V1() set
0. L is V44(L) Element of the carrier of L
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
the carrier of K is non empty set
0. L is V44(L) Element of the carrier of L
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
K109( the U5 of K, the carrier of L) is set
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
K5( the lmult of K,[: the carrier of S, the carrier of L:]) is V1() set
0. ((Omega). L) is V44( (Omega). L) Element of the carrier of ((Omega). L)
the carrier of ((Omega). L) is non empty set
the ZeroF of ((Omega). L) is Element of the carrier of ((Omega). L)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
Subspaces K is set
bool (Subspaces K) is non empty set
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
t is Element of bool (Subspaces K)
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
k is Element of bool (Subspaces K)
x is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
b is Element of bool (Subspaces K)
t is Element of bool (Subspaces K)
b is Element of bool (Subspaces K)
t is Element of bool (Subspaces K)
k is set
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
s is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of b
the carrier of b is non empty set
the U5 of b is V6() V18([: the carrier of b, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]
[: the carrier of b, the carrier of b:] is non empty set
[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
the ZeroF of b is Element of the carrier of b
the lmult of b is V6() V18([: the carrier of S, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of S, the carrier of b:], the carrier of b:]
[: the carrier of S, the carrier of b:] is non empty set
[:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
VectSpStr(# the carrier of b, the U5 of b, the ZeroF of b, the lmult of b #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(S,K,L,a) is Element of bool (Subspaces K)
Subspaces K is set
bool (Subspaces K) is non empty set
(S,K,b,t) is Element of bool (Subspaces K)
k is set
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
k is set
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
Subspaces K is set
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
(S,K,L,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of K
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of b
the carrier of b is non empty set
the U5 of b is V6() V18([: the carrier of b, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]
[: the carrier of b, the carrier of b:] is non empty set
[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
the ZeroF of b is Element of the carrier of b
the lmult of b is V6() V18([: the carrier of S, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of S, the carrier of b:], the carrier of b:]
[: the carrier of S, the carrier of b:] is non empty set
[:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
VectSpStr(# the carrier of b, the U5 of b, the ZeroF of b, the lmult of b #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(S,K,L,a) is Element of bool (Subspaces K)
Subspaces K is set
bool (Subspaces K) is non empty set
(S,K,L,a) is Element of bool (Subspaces K)
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
(S,K,b,t) is Element of bool (Subspaces K)
(S,K,b,t) is Element of bool (Subspaces K)
{((Omega). b),((Omega). t)} is finite set
(S,K,b,t) \ {((Omega). b),((Omega). t)} is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
Subspaces K is set
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(S,K,L,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,L,a) is Element of bool (Subspaces K)
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
b Subspaces_of K is set
(S,K,L,a) /\ (b Subspaces_of K) is Element of bool (Subspaces K)
bool (b Subspaces_of K) is non empty set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(S,K,a,b,L) is Element of bool (L Subspaces_of K)
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
Subspaces K is set
(S,K,a,b) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,a,b) is Element of bool (Subspaces K)
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
(Omega). b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of b
the carrier of b is non empty set
the U5 of b is V6() V18([: the carrier of b, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]
[: the carrier of b, the carrier of b:] is non empty set
[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
the ZeroF of b is Element of the carrier of b
the lmult of b is V6() V18([: the carrier of S, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of S, the carrier of b:], the carrier of b:]
[: the carrier of S, the carrier of b:] is non empty set
[:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
VectSpStr(# the carrier of b, the U5 of b, the ZeroF of b, the lmult of b #) is strict VectSpStr over S
{((Omega). a),((Omega). b)} is finite set
(S,K,a,b) \ {((Omega). a),((Omega). b)} is Element of bool (Subspaces K)
(S,K,a,b) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(Omega). b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of b
the carrier of b is non empty set
the U5 of b is V6() V18([: the carrier of b, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]
[: the carrier of b, the carrier of b:] is non empty set
[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
the ZeroF of b is Element of the carrier of b
the lmult of b is V6() V18([: the carrier of S, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of S, the carrier of b:], the carrier of b:]
[: the carrier of S, the carrier of b:] is non empty set
[:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of S, the carrier of b:], the carrier of b:] is non empty set
VectSpStr(# the carrier of b, the U5 of b, the ZeroF of b, the lmult of b #) is strict VectSpStr over S
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,a,b,L) is Element of bool (L Subspaces_of K)
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
Subspaces K is set
(S,K,a,b) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,a,b) is Element of bool (Subspaces K)
{((Omega). a),((Omega). b)} is finite set
(S,K,a,b) \ {((Omega). a),((Omega). b)} is Element of bool (Subspaces K)
(S,K,a,b) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
(S,K,t,k,L) is Element of bool (L Subspaces_of K)
(S,K,t,k) is Element of bool (Subspaces K)
(S,K,t,k) is Element of bool (Subspaces K)
{((Omega). t),((Omega). k)} is finite set
(S,K,t,k) \ {((Omega). t),((Omega). k)} is Element of bool (Subspaces K)
(S,K,t,k) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
bool (L Subspaces_of K) is non empty Element of bool (bool (L Subspaces_of K))
b is set
t is set
t is Element of bool (bool (L Subspaces_of K))
k is set
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
x is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim y) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,y,x,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,y,x) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,y,x) is Element of bool (Subspaces K)
(Omega). y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of y is non empty set
the U5 of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the ZeroF of y is Element of the carrier of y
the lmult of y is V6() V18([: the carrier of S, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of S, the carrier of y:], the carrier of y:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of y:] is non empty set
[:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
VectSpStr(# the carrier of y, the U5 of y, the ZeroF of y, the lmult of y #) is strict VectSpStr over S
(Omega). x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x
the carrier of x is non empty set
the U5 of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the ZeroF of x is Element of the carrier of x
the lmult of x is V6() V18([: the carrier of S, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of S, the carrier of x:], the carrier of x:]
[: the carrier of S, the carrier of x:] is non empty set
[:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
VectSpStr(# the carrier of x, the U5 of x, the ZeroF of x, the lmult of x #) is strict VectSpStr over S
{((Omega). y),((Omega). x)} is finite set
(S,K,y,x) \ {((Omega). y),((Omega). x)} is Element of bool (Subspaces K)
(S,K,y,x) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
a is Element of bool (bool (L Subspaces_of K))
b is Element of bool (bool (L Subspaces_of K))
t is set
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim k) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,k,y,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,k,y) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,k,y) is Element of bool (Subspaces K)
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
(Omega). y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of y is non empty set
the U5 of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the ZeroF of y is Element of the carrier of y
the lmult of y is V6() V18([: the carrier of S, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of S, the carrier of y:], the carrier of y:]
[: the carrier of S, the carrier of y:] is non empty set
[:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
VectSpStr(# the carrier of y, the U5 of y, the ZeroF of y, the lmult of y #) is strict VectSpStr over S
{((Omega). k),((Omega). y)} is finite set
(S,K,k,y) \ {((Omega). k),((Omega). y)} is Element of bool (Subspaces K)
(S,K,k,y) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim k) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,k,y,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,k,y) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,k,y) is Element of bool (Subspaces K)
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
(Omega). y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of y is non empty set
the U5 of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the ZeroF of y is Element of the carrier of y
the lmult of y is V6() V18([: the carrier of S, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of S, the carrier of y:], the carrier of y:]
[: the carrier of S, the carrier of y:] is non empty set
[:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
VectSpStr(# the carrier of y, the U5 of y, the ZeroF of y, the lmult of y #) is strict VectSpStr over S
{((Omega). k),((Omega). y)} is finite set
(S,K,k,y) \ {((Omega). k),((Omega). y)} is Element of bool (Subspaces K)
(S,K,k,y) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L -' 1 is V21() V22() V23() V27() finite cardinal V51() ext-real non negative V125() Element of NAT
b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
dim b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim b) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(S,K,t,a,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,t,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,t,a) is Element of bool (Subspaces K)
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
{((Omega). t),((Omega). a)} is finite set
(S,K,t,a) \ {((Omega). t),((Omega). a)} is Element of bool (Subspaces K)
(S,K,t,a) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
b /\ t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
b + t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
k + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(S,K,L,a,k) is Element of bool (k Subspaces_of K)
k Subspaces_of K is set
bool (k Subspaces_of K) is non empty set
Subspaces K is set
(S,K,L,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,L,a) is Element of bool (Subspaces K)
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
(S,K,L,a) /\ (k Subspaces_of K) is Element of bool (Subspaces K)
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
x /\ y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (x /\ y) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(Omega). (x /\ y) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x /\ y
the carrier of (x /\ y) is non empty set
the U5 of (x /\ y) is V6() V18([: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y)) Element of bool [:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):]
[: the carrier of (x /\ y), the carrier of (x /\ y):] is non empty set
[:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
bool [:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
the ZeroF of (x /\ y) is Element of the carrier of (x /\ y)
the lmult of (x /\ y) is V6() V18([: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y)) Element of bool [:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):]
[: the carrier of S, the carrier of (x /\ y):] is non empty set
[:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
bool [:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
VectSpStr(# the carrier of (x /\ y), the U5 of (x /\ y), the ZeroF of (x /\ y), the lmult of (x /\ y) #) is strict VectSpStr over S
x + y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (x + y) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim (x + y)) + (dim L) is V51() ext-real V125() set
((dim (x + y)) + (dim L)) - (dim L) is V51() ext-real V125() set
(dim x) + (dim y) is V51() ext-real V125() set
((dim x) + (dim y)) - (dim L) is V51() ext-real V125() set
(Omega). (x + y) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x + y
the carrier of (x + y) is non empty set
the U5 of (x + y) is V6() V18([: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y)) Element of bool [:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):]
[: the carrier of (x + y), the carrier of (x + y):] is non empty set
[:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):] is non empty set
bool [:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):] is non empty set
the ZeroF of (x + y) is Element of the carrier of (x + y)
the lmult of (x + y) is V6() V18([: the carrier of S, the carrier of (x + y):], the carrier of (x + y)) Element of bool [:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):]
[: the carrier of S, the carrier of (x + y):] is non empty set
[:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):] is non empty set
bool [:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):] is non empty set
VectSpStr(# the carrier of (x + y), the U5 of (x + y), the ZeroF of (x + y), the lmult of (x + y) #) is strict VectSpStr over S
(Omega). (x /\ y) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x /\ y
the carrier of (x /\ y) is non empty set
the U5 of (x /\ y) is V6() V18([: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y)) Element of bool [:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):]
[: the carrier of (x /\ y), the carrier of (x /\ y):] is non empty set
[:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
bool [:[: the carrier of (x /\ y), the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
the ZeroF of (x /\ y) is Element of the carrier of (x /\ y)
the lmult of (x /\ y) is V6() V18([: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y)) Element of bool [:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):]
[: the carrier of S, the carrier of (x /\ y):] is non empty set
[:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
bool [:[: the carrier of S, the carrier of (x /\ y):], the carrier of (x /\ y):] is non empty set
VectSpStr(# the carrier of (x /\ y), the U5 of (x /\ y), the ZeroF of (x /\ y), the lmult of (x /\ y) #) is strict VectSpStr over S
(Omega). y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of y is non empty set
the U5 of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the ZeroF of y is Element of the carrier of y
the lmult of y is V6() V18([: the carrier of S, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of S, the carrier of y:], the carrier of y:]
[: the carrier of S, the carrier of y:] is non empty set
[:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
VectSpStr(# the carrier of y, the U5 of y, the ZeroF of y, the lmult of y #) is strict VectSpStr over S
(Omega). x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x
the carrier of x is non empty set
the U5 of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the ZeroF of x is Element of the carrier of x
the lmult of x is V6() V18([: the carrier of S, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of S, the carrier of x:], the carrier of x:]
[: the carrier of S, the carrier of x:] is non empty set
[:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
VectSpStr(# the carrier of x, the U5 of x, the ZeroF of x, the lmult of x #) is strict VectSpStr over S
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
the carrier of K is non empty set
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
L is Element of the carrier of K
{L} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {L} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (Lin {L}) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
0. (Lin {L}) is V44( Lin {L}) Element of the carrier of (Lin {L})
the carrier of (Lin {L}) is non empty set
the ZeroF of (Lin {L}) is Element of the carrier of (Lin {L})
a is Element of the carrier of (Lin {L})
{a} is non empty trivial finite 1 -element Element of bool the carrier of (Lin {L})
bool the carrier of (Lin {L}) is non empty set
Lin {a} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin {L}
(Omega). (Lin {a}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin {a}
the carrier of (Lin {a}) is non empty set
the U5 of (Lin {a}) is V6() V18([: the carrier of (Lin {a}), the carrier of (Lin {a}):], the carrier of (Lin {a})) Element of bool [:[: the carrier of (Lin {a}), the carrier of (Lin {a}):], the carrier of (Lin {a}):]
[: the carrier of (Lin {a}), the carrier of (Lin {a}):] is non empty set
[:[: the carrier of (Lin {a}), the carrier of (Lin {a}):], the carrier of (Lin {a}):] is non empty set
bool [:[: the carrier of (Lin {a}), the carrier of (Lin {a}):], the carrier of (Lin {a}):] is non empty set
the ZeroF of (Lin {a}) is Element of the carrier of (Lin {a})
the lmult of (Lin {a}) is V6() V18([: the carrier of S, the carrier of (Lin {a}):], the carrier of (Lin {a})) Element of bool [:[: the carrier of S, the carrier of (Lin {a}):], the carrier of (Lin {a}):]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of (Lin {a}):] is non empty set
[:[: the carrier of S, the carrier of (Lin {a}):], the carrier of (Lin {a}):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin {a}):], the carrier of (Lin {a}):] is non empty set
VectSpStr(# the carrier of (Lin {a}), the U5 of (Lin {a}), the ZeroF of (Lin {a}), the lmult of (Lin {a}) #) is strict VectSpStr over S
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
the carrier of K is non empty set
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
a is Element of the carrier of K
{a} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {a} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L + (Lin {a}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (L + (Lin {a})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L /\ (Lin {a}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Omega). (L /\ (Lin {a})) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L /\ (Lin {a})
the carrier of (L /\ (Lin {a})) is non empty set
the U5 of (L /\ (Lin {a})) is V6() V18([: the carrier of (L /\ (Lin {a})), the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a}))) Element of bool [:[: the carrier of (L /\ (Lin {a})), the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):]
[: the carrier of (L /\ (Lin {a})), the carrier of (L /\ (Lin {a})):] is non empty set
[:[: the carrier of (L /\ (Lin {a})), the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):] is non empty set
bool [:[: the carrier of (L /\ (Lin {a})), the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):] is non empty set
the ZeroF of (L /\ (Lin {a})) is Element of the carrier of (L /\ (Lin {a}))
the lmult of (L /\ (Lin {a})) is V6() V18([: the carrier of S, the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a}))) Element of bool [:[: the carrier of S, the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of (L /\ (Lin {a})):] is non empty set
[:[: the carrier of S, the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):] is non empty set
bool [:[: the carrier of S, the carrier of (L /\ (Lin {a})):], the carrier of (L /\ (Lin {a})):] is non empty set
VectSpStr(# the carrier of (L /\ (Lin {a})), the U5 of (L /\ (Lin {a})), the ZeroF of (L /\ (Lin {a})), the lmult of (L /\ (Lin {a})) #) is strict VectSpStr over S
the carrier of ((Omega). (L /\ (Lin {a}))) is non empty set
0. (L /\ (Lin {a})) is V44(L /\ (Lin {a})) Element of the carrier of (L /\ (Lin {a}))
{(0. (L /\ (Lin {a})))} is non empty trivial finite 1 -element Element of bool the carrier of (L /\ (Lin {a}))
bool the carrier of (L /\ (Lin {a})) is non empty set
b is set
the carrier of L is non empty set
the carrier of (Lin {a}) is non empty set
the carrier of L /\ the carrier of (Lin {a}) is set
t is Element of the carrier of S
t * a is Element of the carrier of K
0. S is V44(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
t " is Element of the carrier of S
(t ") * (t * a) is Element of the carrier of K
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
b is set
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
(0). (L /\ (Lin {a})) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L /\ (Lin {a})
dim (L /\ (Lin {a})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim (L + (Lin {a}))) + (dim (L /\ (Lin {a}))) is V51() ext-real V125() set
dim (Lin {a}) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + (dim (Lin {a})) is V51() ext-real V125() set
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
the carrier of K is non empty set
(0). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + 2 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
a is Element of the carrier of K
b is Element of the carrier of K
{a,b} is finite Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {a,b} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L /\ (Lin {a,b}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L + (Lin {a,b}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (L + (Lin {a,b})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
the carrier of (Lin {a,b}) is non empty set
bool the carrier of (Lin {a,b}) is non empty set
t is Element of the carrier of (Lin {a,b})
k is Element of the carrier of (Lin {a,b})
{t,k} is finite Element of bool the carrier of (Lin {a,b})
(Omega). (Lin {a,b}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin {a,b}
the U5 of (Lin {a,b}) is V6() V18([: the carrier of (Lin {a,b}), the carrier of (Lin {a,b}):], the carrier of (Lin {a,b})) Element of bool [:[: the carrier of (Lin {a,b}), the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):]
[: the carrier of (Lin {a,b}), the carrier of (Lin {a,b}):] is non empty set
[:[: the carrier of (Lin {a,b}), the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):] is non empty set
bool [:[: the carrier of (Lin {a,b}), the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):] is non empty set
the ZeroF of (Lin {a,b}) is Element of the carrier of (Lin {a,b})
the lmult of (Lin {a,b}) is V6() V18([: the carrier of S, the carrier of (Lin {a,b}):], the carrier of (Lin {a,b})) Element of bool [:[: the carrier of S, the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of (Lin {a,b}):] is non empty set
[:[: the carrier of S, the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin {a,b}):], the carrier of (Lin {a,b}):] is non empty set
VectSpStr(# the carrier of (Lin {a,b}), the U5 of (Lin {a,b}), the ZeroF of (Lin {a,b}), the lmult of (Lin {a,b}) #) is strict VectSpStr over S
y is linearly-independent Element of bool the carrier of (Lin {a,b})
Lin y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin {a,b}
dim (Lin {a,b}) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(Omega). (L /\ (Lin {a,b})) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L /\ (Lin {a,b})
the carrier of (L /\ (Lin {a,b})) is non empty set
the U5 of (L /\ (Lin {a,b})) is V6() V18([: the carrier of (L /\ (Lin {a,b})), the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b}))) Element of bool [:[: the carrier of (L /\ (Lin {a,b})), the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):]
[: the carrier of (L /\ (Lin {a,b})), the carrier of (L /\ (Lin {a,b})):] is non empty set
[:[: the carrier of (L /\ (Lin {a,b})), the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):] is non empty set
bool [:[: the carrier of (L /\ (Lin {a,b})), the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):] is non empty set
the ZeroF of (L /\ (Lin {a,b})) is Element of the carrier of (L /\ (Lin {a,b}))
the lmult of (L /\ (Lin {a,b})) is V6() V18([: the carrier of S, the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b}))) Element of bool [:[: the carrier of S, the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):]
[: the carrier of S, the carrier of (L /\ (Lin {a,b})):] is non empty set
[:[: the carrier of S, the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):] is non empty set
bool [:[: the carrier of S, the carrier of (L /\ (Lin {a,b})):], the carrier of (L /\ (Lin {a,b})):] is non empty set
VectSpStr(# the carrier of (L /\ (Lin {a,b})), the U5 of (L /\ (Lin {a,b})), the ZeroF of (L /\ (Lin {a,b})), the lmult of (L /\ (Lin {a,b})) #) is strict VectSpStr over S
(0). (L /\ (Lin {a,b})) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L /\ (Lin {a,b})
dim (L /\ (Lin {a,b})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim (L + (Lin {a,b}))) + (dim (L /\ (Lin {a,b}))) is V51() ext-real V125() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
the carrier of K is non empty set
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
b + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(S,K,L,a,b) is Element of bool (b Subspaces_of K)
b Subspaces_of K is set
bool (b Subspaces_of K) is non empty set
Subspaces K is set
(S,K,L,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,L,a) is Element of bool (Subspaces K)
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
(S,K,L,a) /\ (b Subspaces_of K) is Element of bool (Subspaces K)
t is Element of the carrier of K
{t} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {t} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L + (Lin {t}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (L + (Lin {t})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
dim ((Omega). a) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
dim ((Omega). L) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim ((Omega). L)) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
a is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim L) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
t is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
t + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(S,K,L,a,t) is Element of bool (t Subspaces_of K)
t Subspaces_of K is set
bool (t Subspaces_of K) is non empty set
Subspaces K is set
(S,K,L,a) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,L,a) is Element of bool (Subspaces K)
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
(Omega). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the carrier of a is non empty set
the U5 of a is V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the ZeroF of a is Element of the carrier of a
the lmult of a is V6() V18([: the carrier of S, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of S, the carrier of a:], the carrier of a:]
[: the carrier of S, the carrier of a:] is non empty set
[:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of S, the carrier of a:], the carrier of a:] is non empty set
VectSpStr(# the carrier of a, the U5 of a, the ZeroF of a, the lmult of a #) is strict VectSpStr over S
{((Omega). L),((Omega). a)} is finite set
(S,K,L,a) \ {((Omega). L),((Omega). a)} is Element of bool (Subspaces K)
(S,K,L,a) /\ (t Subspaces_of K) is Element of bool (Subspaces K)
b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b /\ b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
(0). a is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
dim b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
dim the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim b) + (dim the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b) is V51() ext-real V125() set
the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is non empty set
(Omega). the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is V6() V18([: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b) Element of bool [:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:]
[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
[:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
bool [:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is V6() V18([: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b) Element of bool [:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:]
[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
[:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
bool [:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b:] is non empty set
VectSpStr(# the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b, the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b #) is strict VectSpStr over S
y is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
x is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
{y,x} is finite Element of bool the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
bool the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is non empty set
Lin {y,x} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
{y} is non empty trivial finite 1 -element Element of bool the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
Lin {y} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
s is Element of the carrier of S
s * y is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
the carrier of K is non empty set
s is Element of the carrier of a
l is Element of the carrier of a
0. a is V44(a) Element of the carrier of a
0. the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b is V44( the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b) Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of b
w is Element of the carrier of K
{w} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {w} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L + (Lin {w}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
{s} is non empty trivial finite 1 -element Element of bool the carrier of a
bool the carrier of a is non empty set
Lin {s} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of a
z is Element of the carrier of K
{z} is non empty trivial finite 1 -element Element of bool the carrier of K
Lin {z} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
L + (Lin {z}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
x is Element of the carrier of K
y is Element of the carrier of K
x + y is Element of the carrier of K
y9 is Element of the carrier of S
y9 * z is Element of the carrier of K
w - (y9 * z) is Element of the carrier of K
- (y9 * z) is Element of the carrier of K
K146(K,w,(- (y9 * z))) is Element of the carrier of K
(y9 * z) - (y9 * z) is Element of the carrier of K
K146(K,(y9 * z),(- (y9 * z))) is Element of the carrier of K
x + ((y9 * z) - (y9 * z)) is Element of the carrier of K
0. K is V44(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
x + (0. K) is Element of the carrier of K
y9 * s is Element of the carrier of a
l - (y9 * s) is Element of the carrier of a
- (y9 * s) is Element of the carrier of a
K146(a,l,(- (y9 * s))) is Element of the carrier of a
X is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
card (S,K,L,a,t) is V21() V22() V23() cardinal set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is strict TopStruct
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
the topology of (S,K,L) is Element of bool (bool the carrier of (S,K,L))
the carrier of (S,K,L) is set
bool the carrier of (S,K,L) is non empty set
bool (bool the carrier of (S,K,L)) is non empty set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is strict TopStruct
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
the topology of (S,K,L) is Element of bool (bool the carrier of (S,K,L))
the carrier of (S,K,L) is set
bool the carrier of (S,K,L) is non empty set
bool (bool the carrier of (S,K,L)) is non empty set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
b is Element of the topology of (S,K,L)
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim t is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim t) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,t,k,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,t,k) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,t,k) is Element of bool (Subspaces K)
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
{((Omega). t),((Omega). k)} is finite set
(S,K,t,k) \ {((Omega). t),((Omega). k)} is Element of bool (Subspaces K)
(S,K,t,k) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
the carrier of K is non empty set
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
y is set
x is Element of the carrier of K
{x} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
Lin {x} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
t + (Lin {x}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of (t + (Lin {x})) is non empty set
dim (t + (Lin {x})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
the Basis of t is Basis of t
bool the carrier of t is non empty set
2 - 1 is V51() ext-real V125() set
((dim t) + 1) - 1 is V51() ext-real V125() set
x is finite Element of bool the carrier of t
card x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
s is set
bool the carrier of K is non empty set
l is Element of the carrier of t
{l} is non empty trivial finite 1 -element Element of bool the carrier of t
x \ {l} is finite Element of bool the carrier of t
the Basis of t \ {l} is Element of bool the carrier of t
z is finite Element of bool the carrier of K
Lin z is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of (Lin z) is non empty set
X is set
bool the carrier of (Lin z) is non empty set
w is linearly-independent Element of bool the carrier of K
X is linearly-independent Element of bool the carrier of (Lin z)
Lin X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin z
card the Basis of t is V21() V22() V23() cardinal set
the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
t /\ the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(0). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(L + 1) - ((dim t) + 1) is V51() ext-real V125() set
dim the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim t) + (dim the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t) is V51() ext-real V125() set
((dim t) + (dim the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t)) - ((dim t) + 1) is V51() ext-real V125() set
the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is non empty set
(Omega). the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is V6() V18([: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t) Element of bool [:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:]
[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
[:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
bool [:[: the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is V6() V18([: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t) Element of bool [:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:]
[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
[:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
bool [:[: the carrier of S, the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:], the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t:] is non empty set
VectSpStr(# the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t #) is strict VectSpStr over S
y is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
y9 is Element of the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
{y,y9} is finite Element of bool the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
bool the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t is non empty set
Lin {y,y9} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t
Y is linearly-independent Element of bool the carrier of K
Lin ( the Basis of t \ {l}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
Lin the Basis of t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
x9 is Element of the carrier of K
II2 is Element of the carrier of K
{x9,II2} is finite Element of bool the carrier of K
Lin {x9,II2} is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Lin z) /\ (Lin {x9,II2}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of ((Lin z) /\ (Lin {x9,II2})) is non empty set
the carrier of ((0). K) is non empty set
IV is set
the carrier of VectSpStr(# the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t #) is set
card z is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card {l} is non empty V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(card x) - (card {l}) is V51() ext-real V125() set
(dim t) - 1 is V51() ext-real V125() set
dim (Lin z) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(Lin z) + (Lin {x9,II2}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim ((Lin z) + (Lin {x9,II2})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
((dim t) - 1) + 2 is V51() ext-real V125() set
IV is Element of bool the carrier of K
the carrier of ((Lin z) + (Lin {x9,II2})) is non empty set
a is set
( the Basis of t \ {l}) \/ {l} is Element of bool the carrier of t
o is Element of the carrier of K
Lin IV is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
t /\ (Lin {x9,II2}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of (t /\ (Lin {x9,II2})) is non empty set
a is set
the carrier of VectSpStr(# the carrier of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the U5 of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the ZeroF of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t, the lmult of the non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Linear_Compl of t #) is set
t + (Lin {x9,II2}) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (t + (Lin {x9,II2})) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim t) + 2 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
((dim t) + 1) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is strict TopStruct
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
the topology of (S,K,L) is Element of bool (bool the carrier of (S,K,L))
the carrier of (S,K,L) is set
bool the carrier of (S,K,L) is non empty set
bool (bool the carrier of (S,K,L)) is non empty set
b is Element of the topology of (S,K,L)
card b is V21() V22() V23() cardinal set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim t is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim t) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,t,k,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,t,k) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,t,k) is Element of bool (Subspaces K)
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
{((Omega). t),((Omega). k)} is finite set
(S,K,t,k) \ {((Omega). t),((Omega). k)} is Element of bool (Subspaces K)
(S,K,t,k) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is strict TopStruct
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
the topology of (S,K,L) is Element of bool (bool the carrier of (S,K,L))
the carrier of (S,K,L) is set
bool the carrier of (S,K,L) is non empty set
bool (bool the carrier of (S,K,L)) is non empty set
b is Element of the topology of (S,K,L)
t is Element of the topology of (S,K,L)
b /\ t is set
card (b /\ t) is V21() V22() V23() cardinal set
k is set
y is set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
x is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
s is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim x) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim s is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,x,s,L) is Element of bool (L Subspaces_of K)
Subspaces K is set
(S,K,x,s) is Element of bool (Subspaces K)
bool (Subspaces K) is non empty set
(S,K,x,s) is Element of bool (Subspaces K)
(Omega). x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x
the carrier of x is non empty set
the U5 of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the ZeroF of x is Element of the carrier of x
the lmult of x is V6() V18([: the carrier of S, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of S, the carrier of x:], the carrier of x:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of x:] is non empty set
[:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
VectSpStr(# the carrier of x, the U5 of x, the ZeroF of x, the lmult of x #) is strict VectSpStr over S
(Omega). s is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of s
the carrier of s is non empty set
the U5 of s is V6() V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the ZeroF of s is Element of the carrier of s
the lmult of s is V6() V18([: the carrier of S, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of S, the carrier of s:], the carrier of s:]
[: the carrier of S, the carrier of s:] is non empty set
[:[: the carrier of S, the carrier of s:], the carrier of s:] is non empty set
bool [:[: the carrier of S, the carrier of s:], the carrier of s:] is non empty set
VectSpStr(# the carrier of s, the U5 of s, the ZeroF of s, the lmult of s #) is strict VectSpStr over S
{((Omega). x),((Omega). s)} is finite set
(S,K,x,s) \ {((Omega). x),((Omega). s)} is Element of bool (Subspaces K)
(S,K,x,s) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
l is Element of the carrier of (S,K,L)
X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim X is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
z is Element of the carrier of (S,K,L)
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
x is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(dim x) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,x,y,L) is Element of bool (L Subspaces_of K)
(S,K,x,y) is Element of bool (Subspaces K)
(S,K,x,y) is Element of bool (Subspaces K)
(Omega). x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x
the carrier of x is non empty set
the U5 of x is V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the ZeroF of x is Element of the carrier of x
the lmult of x is V6() V18([: the carrier of S, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of S, the carrier of x:], the carrier of x:]
[: the carrier of S, the carrier of x:] is non empty set
[:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of S, the carrier of x:], the carrier of x:] is non empty set
VectSpStr(# the carrier of x, the U5 of x, the ZeroF of x, the lmult of x #) is strict VectSpStr over S
(Omega). y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of y is non empty set
the U5 of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
the ZeroF of y is Element of the carrier of y
the lmult of y is V6() V18([: the carrier of S, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of S, the carrier of y:], the carrier of y:]
[: the carrier of S, the carrier of y:] is non empty set
[:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of S, the carrier of y:], the carrier of y:] is non empty set
VectSpStr(# the carrier of y, the U5 of y, the ZeroF of y, the lmult of y #) is strict VectSpStr over S
{((Omega). x),((Omega). y)} is finite set
(S,K,x,y) \ {((Omega). x),((Omega). y)} is Element of bool (Subspaces K)
(S,K,x,y) /\ (L Subspaces_of K) is Element of bool (Subspaces K)
w is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
w + X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
w /\ X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L) is strict TopStruct
L Subspaces_of K is set
(S,K,L) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L) #) is strict TopStruct
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
bool (L Subspaces_of K) is non empty Element of bool (bool (L Subspaces_of K))
t is set
k is set
k is Element of bool (bool (L Subspaces_of K))
y is set
x is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of x is set
b is Element of bool (bool (L Subspaces_of K))
t is Element of bool (bool (L Subspaces_of K))
k is set
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of y is set
y is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of y is set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L,a) is Element of bool (bool (L Subspaces_of K))
L Subspaces_of K is set
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
b is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim b is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of b is set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of K is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a Subspaces_of K is set
a Subspaces_of L is set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of K is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
L is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
(Omega). L is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
the carrier of L is non empty set
the U5 of L is V6() V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is Element of the carrier of L
the lmult of L is V6() V18([: the carrier of S, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of S, the carrier of L:], the carrier of L:]
[: the carrier of S, the carrier of L:] is non empty set
[:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of S, the carrier of L:], the carrier of L:] is non empty set
VectSpStr(# the carrier of L, the U5 of L, the ZeroF of L, the lmult of L #) is strict VectSpStr over S
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a Subspaces_of K is set
a Subspaces_of L is set
dim L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
b is set
0. K is V44(K) Element of the carrier of K
t is Element of the carrier of K
{t} is non empty trivial finite 1 -element Element of bool the carrier of K
bool the carrier of K is non empty set
k is Basis of K
y is finite Element of bool the carrier of K
card y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
bool y is non empty finite V32() set
x is finite Element of bool y
card x is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
s is finite Element of bool the carrier of K
Lin s is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of (Lin s) is non empty set
l is set
bool the carrier of (Lin s) is non empty set
l is Element of bool the carrier of (Lin s)
z is linearly-independent Element of bool the carrier of (Lin s)
Lin z is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin s
the U5 of (Lin s) is V6() V18([: the carrier of (Lin s), the carrier of (Lin s):], the carrier of (Lin s)) Element of bool [:[: the carrier of (Lin s), the carrier of (Lin s):], the carrier of (Lin s):]
[: the carrier of (Lin s), the carrier of (Lin s):] is non empty set
[:[: the carrier of (Lin s), the carrier of (Lin s):], the carrier of (Lin s):] is non empty set
bool [:[: the carrier of (Lin s), the carrier of (Lin s):], the carrier of (Lin s):] is non empty set
the ZeroF of (Lin s) is Element of the carrier of (Lin s)
the lmult of (Lin s) is V6() V18([: the carrier of S, the carrier of (Lin s):], the carrier of (Lin s)) Element of bool [:[: the carrier of S, the carrier of (Lin s):], the carrier of (Lin s):]
[: the carrier of S, the carrier of (Lin s):] is non empty set
[:[: the carrier of S, the carrier of (Lin s):], the carrier of (Lin s):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin s):], the carrier of (Lin s):] is non empty set
VectSpStr(# the carrier of (Lin s), the U5 of (Lin s), the ZeroF of (Lin s), the lmult of (Lin s) #) is strict VectSpStr over S
dim (Lin s) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
w is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
dim w is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
s is set
{s} is non empty trivial finite 1 -element set
x \ {s} is finite Element of bool y
(x \ {s}) \/ {t} is finite set
l is set
l is finite Element of bool the carrier of K
Lin l is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of (Lin l) is non empty set
z is set
bool the carrier of (Lin l) is non empty set
w is set
z is Element of bool the carrier of (Lin l)
w is linearly-independent Element of bool the carrier of (Lin l)
Lin w is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin l
the U5 of (Lin l) is V6() V18([: the carrier of (Lin l), the carrier of (Lin l):], the carrier of (Lin l)) Element of bool [:[: the carrier of (Lin l), the carrier of (Lin l):], the carrier of (Lin l):]
[: the carrier of (Lin l), the carrier of (Lin l):] is non empty set
[:[: the carrier of (Lin l), the carrier of (Lin l):], the carrier of (Lin l):] is non empty set
bool [:[: the carrier of (Lin l), the carrier of (Lin l):], the carrier of (Lin l):] is non empty set
the ZeroF of (Lin l) is Element of the carrier of (Lin l)
the lmult of (Lin l) is V6() V18([: the carrier of S, the carrier of (Lin l):], the carrier of (Lin l)) Element of bool [:[: the carrier of S, the carrier of (Lin l):], the carrier of (Lin l):]
[: the carrier of S, the carrier of (Lin l):] is non empty set
[:[: the carrier of S, the carrier of (Lin l):], the carrier of (Lin l):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin l):], the carrier of (Lin l):] is non empty set
VectSpStr(# the carrier of (Lin l), the U5 of (Lin l), the ZeroF of (Lin l), the lmult of (Lin l) #) is strict VectSpStr over S
card l is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card (x \ {s}) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(card (x \ {s})) + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card {s} is non empty V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(card x) - (card {s}) is V51() ext-real V125() set
((card x) - (card {s})) + 1 is V51() ext-real V125() set
(card x) - 1 is V51() ext-real V125() set
((card x) - 1) + 1 is V51() ext-real V125() set
dim (Lin l) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of L
dim X is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of K is set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L,a) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,a) #) is strict TopStruct
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L,a) is strict TopStruct
L Subspaces_of K is set
(S,K,L,a) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,a) #) is strict TopStruct
the topology of (S,K,L,a) is Element of bool (bool the carrier of (S,K,L,a))
the carrier of (S,K,L,a) is set
bool the carrier of (S,K,L,a) is non empty set
bool (bool the carrier of (S,K,L,a)) is non empty set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L,a) is strict TopStruct
L Subspaces_of K is set
(S,K,L,a) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,a) #) is strict TopStruct
the carrier of (S,K,L,a) is set
the topology of (S,K,L,a) is Element of bool (bool the carrier of (S,K,L,a))
bool the carrier of (S,K,L,a) is non empty set
bool (bool the carrier of (S,K,L,a)) is non empty set
t is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim t is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of t is set
(Omega). K is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
the carrier of K is non empty set
the U5 of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the ZeroF of K is Element of the carrier of K
the lmult of K is V6() V18([: the carrier of S, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of S, the carrier of K:], the carrier of K:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of K:] is non empty set
[:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of S, the carrier of K:], the carrier of K:] is non empty set
VectSpStr(# the carrier of K, the U5 of K, the ZeroF of K, the lmult of K #) is strict VectSpStr over S
(Omega). t is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of t
the carrier of t is non empty set
the U5 of t is V6() V18([: the carrier of t, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of t, the carrier of t:], the carrier of t:]
[: the carrier of t, the carrier of t:] is non empty set
[:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of t, the carrier of t:], the carrier of t:] is non empty set
the ZeroF of t is Element of the carrier of t
the lmult of t is V6() V18([: the carrier of S, the carrier of t:], the carrier of t) Element of bool [:[: the carrier of S, the carrier of t:], the carrier of t:]
[: the carrier of S, the carrier of t:] is non empty set
[:[: the carrier of S, the carrier of t:], the carrier of t:] is non empty set
bool [:[: the carrier of S, 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 S
dim ((Omega). K) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
a is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
(S,K,L,a) is strict TopStruct
L Subspaces_of K is set
(S,K,L,a) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,a) #) is strict TopStruct
the topology of (S,K,L,a) is Element of bool (bool the carrier of (S,K,L,a))
the carrier of (S,K,L,a) is set
bool the carrier of (S,K,L,a) is non empty set
bool (bool the carrier of (S,K,L,a)) is non empty set
t is Element of the topology of (S,K,L,a)
card t is V21() V22() V23() cardinal set
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of k is set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
dim y is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
the Basis of y is Basis of y
card the Basis of y is V21() V22() V23() cardinal set
the carrier of y is non empty set
bool the carrier of y is non empty set
1 + 1 is non empty V21() V22() V23() V27() finite cardinal V51() ext-real positive non negative V125() Element of NAT
l is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
l + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
z is set
w is set
s is finite Element of bool the carrier of y
{z} is non empty trivial finite 1 -element set
s \ {z} is finite Element of bool the carrier of y
X is finite Element of bool the carrier of y
Lin X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of (Lin X) is non empty set
x is set
bool the carrier of (Lin X) is non empty set
x is Element of bool the carrier of (Lin X)
y is linearly-independent Element of bool the carrier of (Lin X)
Lin y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin X
the U5 of (Lin X) is V6() V18([: the carrier of (Lin X), the carrier of (Lin X):], the carrier of (Lin X)) Element of bool [:[: the carrier of (Lin X), the carrier of (Lin X):], the carrier of (Lin X):]
[: the carrier of (Lin X), the carrier of (Lin X):] is non empty set
[:[: the carrier of (Lin X), the carrier of (Lin X):], the carrier of (Lin X):] is non empty set
bool [:[: the carrier of (Lin X), the carrier of (Lin X):], the carrier of (Lin X):] is non empty set
the ZeroF of (Lin X) is Element of the carrier of (Lin X)
the lmult of (Lin X) is V6() V18([: the carrier of S, the carrier of (Lin X):], the carrier of (Lin X)) Element of bool [:[: the carrier of S, the carrier of (Lin X):], the carrier of (Lin X):]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of (Lin X):] is non empty set
[:[: the carrier of S, the carrier of (Lin X):], the carrier of (Lin X):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin X):], the carrier of (Lin X):] is non empty set
VectSpStr(# the carrier of (Lin X), the U5 of (Lin X), the ZeroF of (Lin X), the lmult of (Lin X) #) is strict VectSpStr over S
{w} is non empty trivial finite 1 -element set
s \ {w} is finite Element of bool the carrier of y
y9 is finite Element of bool the carrier of y
Lin y9 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y
the carrier of (Lin y9) is non empty set
x9 is set
bool the carrier of (Lin y9) is non empty set
x9 is Element of bool the carrier of (Lin y9)
II2 is linearly-independent Element of bool the carrier of (Lin y9)
Lin II2 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of Lin y9
the U5 of (Lin y9) is V6() V18([: the carrier of (Lin y9), the carrier of (Lin y9):], the carrier of (Lin y9)) Element of bool [:[: the carrier of (Lin y9), the carrier of (Lin y9):], the carrier of (Lin y9):]
[: the carrier of (Lin y9), the carrier of (Lin y9):] is non empty set
[:[: the carrier of (Lin y9), the carrier of (Lin y9):], the carrier of (Lin y9):] is non empty set
bool [:[: the carrier of (Lin y9), the carrier of (Lin y9):], the carrier of (Lin y9):] is non empty set
the ZeroF of (Lin y9) is Element of the carrier of (Lin y9)
the lmult of (Lin y9) is V6() V18([: the carrier of S, the carrier of (Lin y9):], the carrier of (Lin y9)) Element of bool [:[: the carrier of S, the carrier of (Lin y9):], the carrier of (Lin y9):]
[: the carrier of S, the carrier of (Lin y9):] is non empty set
[:[: the carrier of S, the carrier of (Lin y9):], the carrier of (Lin y9):] is non empty set
bool [:[: the carrier of S, the carrier of (Lin y9):], the carrier of (Lin y9):] is non empty set
VectSpStr(# the carrier of (Lin y9), the U5 of (Lin y9), the ZeroF of (Lin y9), the lmult of (Lin y9) #) is strict VectSpStr over S
card y9 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card s is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card {w} is non empty V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(card s) - (card {w}) is V51() ext-real V125() set
(l + 1) - 1 is V51() ext-real V125() set
dim (Lin y9) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
card X is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
card {z} is non empty V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(card s) - (card {z}) is V51() ext-real V125() set
dim (Lin X) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(S,K,L,(L + 1)) is strict TopStruct
L Subspaces_of K is set
(S,K,L,(L + 1)) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,(L + 1)) #) is strict TopStruct
the topology of (S,K,L,(L + 1)) is Element of bool (bool the carrier of (S,K,L,(L + 1)))
the carrier of (S,K,L,(L + 1)) is set
bool the carrier of (S,K,L,(L + 1)) is non empty set
bool (bool the carrier of (S,K,L,(L + 1))) is non empty set
b is Element of the topology of (S,K,L,(L + 1))
t is Element of the topology of (S,K,L,(L + 1))
b /\ t is set
card (b /\ t) is V21() V22() V23() cardinal set
k is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim k is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of k is set
y is set
x is set
s is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
dim s is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
l is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim l is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L Subspaces_of l is set
z is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of l
dim z is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
w is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of l
dim w is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
X is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
dim X is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
x + y is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
dim (x + y) is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
x9 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x + y
(Omega). x9 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x9
the carrier of x9 is non empty set
the U5 of x9 is V6() V18([: the carrier of x9, the carrier of x9:], the carrier of x9) Element of bool [:[: the carrier of x9, the carrier of x9:], the carrier of x9:]
[: the carrier of x9, the carrier of x9:] is non empty set
[:[: the carrier of x9, the carrier of x9:], the carrier of x9:] is non empty set
bool [:[: the carrier of x9, the carrier of x9:], the carrier of x9:] is non empty set
the ZeroF of x9 is Element of the carrier of x9
the lmult of x9 is V6() V18([: the carrier of S, the carrier of x9:], the carrier of x9) Element of bool [:[: the carrier of S, the carrier of x9:], the carrier of x9:]
the carrier of S is non empty non trivial set
[: the carrier of S, the carrier of x9:] is non empty set
[:[: the carrier of S, the carrier of x9:], the carrier of x9:] is non empty set
bool [:[: the carrier of S, the carrier of x9:], the carrier of x9:] is non empty set
VectSpStr(# the carrier of x9, the U5 of x9, the ZeroF of x9, the lmult of x9 #) is strict VectSpStr over S
(Omega). (x + y) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x + y
the carrier of (x + y) is non empty set
the U5 of (x + y) is V6() V18([: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y)) Element of bool [:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):]
[: the carrier of (x + y), the carrier of (x + y):] is non empty set
[:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):] is non empty set
bool [:[: the carrier of (x + y), the carrier of (x + y):], the carrier of (x + y):] is non empty set
the ZeroF of (x + y) is Element of the carrier of (x + y)
the lmult of (x + y) is V6() V18([: the carrier of S, the carrier of (x + y):], the carrier of (x + y)) Element of bool [:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):]
[: the carrier of S, the carrier of (x + y):] is non empty set
[:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):] is non empty set
bool [:[: the carrier of S, the carrier of (x + y):], the carrier of (x + y):] is non empty set
VectSpStr(# the carrier of (x + y), the U5 of (x + y), the ZeroF of (x + y), the lmult of (x + y) #) is strict VectSpStr over S
y + x is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of K
y9 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of x + y
(Omega). y9 is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of y9
the carrier of y9 is non empty set
the U5 of y9 is V6() V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
the ZeroF of y9 is Element of the carrier of y9
the lmult of y9 is V6() V18([: the carrier of S, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of S, the carrier of y9:], the carrier of y9:]
[: the carrier of S, the carrier of y9:] is non empty set
[:[: the carrier of S, the carrier of y9:], the carrier of y9:] is non empty set
bool [:[: the carrier of S, the carrier of y9:], the carrier of y9:] is non empty set
VectSpStr(# the carrier of y9, the U5 of y9, the ZeroF of y9, the lmult of y9 #) is strict VectSpStr over S
w + z is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of l
(Omega). (w + z) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of w + z
the carrier of (w + z) is non empty set
the U5 of (w + z) is V6() V18([: the carrier of (w + z), the carrier of (w + z):], the carrier of (w + z)) Element of bool [:[: the carrier of (w + z), the carrier of (w + z):], the carrier of (w + z):]
[: the carrier of (w + z), the carrier of (w + z):] is non empty set
[:[: the carrier of (w + z), the carrier of (w + z):], the carrier of (w + z):] is non empty set
bool [:[: the carrier of (w + z), the carrier of (w + z):], the carrier of (w + z):] is non empty set
the ZeroF of (w + z) is Element of the carrier of (w + z)
the lmult of (w + z) is V6() V18([: the carrier of S, the carrier of (w + z):], the carrier of (w + z)) Element of bool [:[: the carrier of S, the carrier of (w + z):], the carrier of (w + z):]
[: the carrier of S, the carrier of (w + z):] is non empty set
[:[: the carrier of S, the carrier of (w + z):], the carrier of (w + z):] is non empty set
bool [:[: the carrier of S, the carrier of (w + z):], the carrier of (w + z):] is non empty set
VectSpStr(# the carrier of (w + z), the U5 of (w + z), the ZeroF of (w + z), the lmult of (w + z) #) is strict VectSpStr over S
(Omega). l is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of l
the carrier of l is non empty set
the U5 of l is V6() V18([: the carrier of l, the carrier of l:], the carrier of l) Element of bool [:[: the carrier of l, the carrier of l:], the carrier of l:]
[: the carrier of l, the carrier of l:] is non empty set
[:[: the carrier of l, the carrier of l:], the carrier of l:] is non empty set
bool [:[: the carrier of l, the carrier of l:], the carrier of l:] is non empty set
the ZeroF of l is Element of the carrier of l
the lmult of l is V6() V18([: the carrier of S, the carrier of l:], the carrier of l) Element of bool [:[: the carrier of S, the carrier of l:], the carrier of l:]
[: the carrier of S, the carrier of l:] is non empty set
[:[: the carrier of S, the carrier of l:], the carrier of l:] is non empty set
bool [:[: the carrier of S, the carrier of l:], the carrier of l:] is non empty set
VectSpStr(# the carrier of l, the U5 of l, the ZeroF of l, the lmult of l #) is strict VectSpStr over S
X + s is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
(Omega). (X + s) is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of X + s
the carrier of (X + s) is non empty set
the U5 of (X + s) is V6() V18([: the carrier of (X + s), the carrier of (X + s):], the carrier of (X + s)) Element of bool [:[: the carrier of (X + s), the carrier of (X + s):], the carrier of (X + s):]
[: the carrier of (X + s), the carrier of (X + s):] is non empty set
[:[: the carrier of (X + s), the carrier of (X + s):], the carrier of (X + s):] is non empty set
bool [:[: the carrier of (X + s), the carrier of (X + s):], the carrier of (X + s):] is non empty set
the ZeroF of (X + s) is Element of the carrier of (X + s)
the lmult of (X + s) is V6() V18([: the carrier of S, the carrier of (X + s):], the carrier of (X + s)) Element of bool [:[: the carrier of S, the carrier of (X + s):], the carrier of (X + s):]
[: the carrier of S, the carrier of (X + s):] is non empty set
[:[: the carrier of S, the carrier of (X + s):], the carrier of (X + s):] is non empty set
bool [:[: the carrier of S, the carrier of (X + s):], the carrier of (X + s):] is non empty set
VectSpStr(# the carrier of (X + s), the U5 of (X + s), the ZeroF of (X + s), the lmult of (X + s) #) is strict VectSpStr over S
(Omega). k is non empty V65() strict V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional Subspace of k
the carrier of k is non empty set
the U5 of k is V6() V18([: the carrier of k, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]
[: the carrier of k, the carrier of k:] is non empty set
[:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set
the ZeroF of k is Element of the carrier of k
the lmult of k is V6() V18([: the carrier of S, the carrier of k:], the carrier of k) Element of bool [:[: the carrier of S, the carrier of k:], the carrier of k:]
[: the carrier of S, the carrier of k:] is non empty set
[:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
bool [:[: the carrier of S, the carrier of k:], the carrier of k:] is non empty set
VectSpStr(# the carrier of k, the U5 of k, the ZeroF of k, the lmult of k #) is strict VectSpStr over S
S is non empty non degenerated non trivial V65() V85() V91() V93() well-unital V99() V112() V113() V114() L11()
K is non empty V65() V102(S) V103(S) V104(S) V105(S) V112() V113() V114() finite-dimensional VectSpStr over S
dim K is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L is V21() V22() V23() V27() finite cardinal V51() ext-real V125() set
L + 1 is V21() V22() V23() V27() finite cardinal V51() ext-real V125() Element of NAT
(S,K,L,(L + 1)) is strict TopStruct
L Subspaces_of K is set
(S,K,L,(L + 1)) is Element of bool (bool (L Subspaces_of K))
bool (L Subspaces_of K) is non empty set
bool (bool (L Subspaces_of K)) is non empty set
TopStruct(# (L Subspaces_of K),(S,K,L,(L + 1)) #) is strict TopStruct
S is set
bool S is non empty Element of bool (bool S)
bool S is non empty set
bool (bool S) is non empty set
K is set
L is set
a is set
b is set
{a,b} is finite set
a is set
b is set
{a,b} is finite set
K is set
L is set
a is set
b is set
t is set
{b,t} is finite set
b is set
t is set
{b,t} is finite set
S is non empty set
(S) is set
K is set
{K,K} is finite set
K is set
S is set
{S} is non empty trivial finite 1 -element set
K \/ {S} is set
bool (K \/ {S}) is non empty Element of bool (bool (K \/ {S}))
bool (K \/ {S}) is non empty set
bool (bool (K \/ {S})) is non empty set
L is set
a is set
b is set
{S,b} is finite set
b is set
{S,b} is finite set
t is set
{S,t} is finite set
L is set
a is set
b is set
t is set
{S,t} is finite set
t is set
{S,t} is finite set
S is set
K is non empty set
(S,K) is set
L is set
{S,L} is finite set
S is set
K is non trivial set
(S,K) is set
card K is V21() V22() V23() cardinal set
L is set
a is set
{S,L} is finite set
{S,a} is finite set
card (S,K) is V21() V22() V23() cardinal set
S is set
bool S is non empty set
bool (bool S) is non empty set
(S) is set
bool (S) is non empty set
bool (bool (S)) is non empty set
K is Element of bool (bool S)
a is Element of bool (bool (S))
b is set
t is set
k is Element of bool S
(t,k) is set
y is set
x is set
{t,x} is finite set
L is Element of bool (bool (S))
a is Element of bool (bool (S))
b is set
t is set
k is Element of bool S
(t,k) is set
t is set
k is Element of bool S
(t,k) is set
S is non empty set
bool S is non empty set
bool (bool S) is non empty set
K is non empty Element of bool (bool S)
(S,K) is Element of bool (bool (S))
(S) is non empty set
bool (S) is non empty set
bool (bool (S)) is non empty set
L is set
a is set
(a,L) is set
S is TopStruct
the carrier of S is set
( the carrier of S) is set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
S is non empty TopStruct
(S) is strict TopStruct
the carrier of S is non empty set
( the carrier of S) is non empty set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
S is non empty non void TopStruct
(S) is non empty strict TopStruct
the carrier of S is non empty set
( the carrier of S) is non empty set
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is non empty Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
the topology of (S) is Element of bool (bool the carrier of (S))
the carrier of (S) is non empty set
bool the carrier of (S) is non empty set
bool (bool the carrier of (S)) is non empty set
S is non empty non void non degenerated TopStruct
(S) is non empty strict non void TopStruct
the carrier of S is non empty set
( the carrier of S) is non empty set
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is non empty Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
the carrier of (S) is non empty set
the topology of (S) is non empty Element of bool (bool the carrier of (S))
bool the carrier of (S) is non empty set
bool (bool the carrier of (S)) is non empty set
K is set
L is Element of bool the carrier of S
(K,L) is set
a is set
{K,a} is finite set
b is set
{K,b} is finite set
b is set
{K,b} is finite set
S is non empty non void with_non_trivial_blocks TopStruct
(S) is non empty strict non void TopStruct
the carrier of S is non empty set
( the carrier of S) is non empty set
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is non empty Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
the topology of (S) is non empty Element of bool (bool the carrier of (S))
the carrier of (S) is non empty set
bool the carrier of (S) is non empty set
bool (bool the carrier of (S)) is non empty set
K is Element of the topology of (S)
card K is V21() V22() V23() cardinal set
L is set
a is Element of bool the carrier of S
(L,a) is set
card a is V21() V22() V23() cardinal set
b is non trivial set
(L,b) is non trivial set
S is identifying_close_blocks TopStruct
(S) is strict TopStruct
the carrier of S is set
( the carrier of S) is set
the topology of S is Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
( the carrier of S, the topology of S) is Element of bool (bool ( the carrier of S))
bool ( the carrier of S) is non empty set
bool (bool ( the carrier of S)) is non empty set
TopStruct(# ( the carrier of S),( the carrier of S, the topology of S) #) is strict TopStruct
the topology of (S) is Element of bool (bool the carrier of (S))
the carrier of (S) is set
bool the carrier of (S) is non empty set
bool (bool the carrier of (S)) is non empty set
K is Element of the topology of (S)
L is Element of the topology of (S)
K /\ L is set
card (K /\ L) is V21() V22() V23() cardinal set
a is set
b is set
t is set
k is Element of bool the carrier of S
(t,k) is set
y is set
{t,y} is finite set
x is set
{t,x} is finite set
s is set
l is Element of bool the carrier of S
(s,l) is set
z is set
{s,z} is finite set
w is set
{s,w} is finite set
k /\ l is Element of bool the carrier of S
card (k /\ l) is V21() V22() V23() cardinal set