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