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