:: HAHNBAN semantic presentation

REAL is non empty V36() V37() V38() V42() V48() set
NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V36() V42() V48() set
ExtREAL is non empty V37() set
omega is V36() V37() V38() V39() V40() V41() V42() set
bool omega is non empty set
RAT is non empty V36() V37() V38() V39() V42() V48() set
INT is non empty V36() V37() V38() V39() V40() V42() V48() set
bool NAT is non empty set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() V38() V39() V40() V41() V42() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() V38() V39() V40() V41() V42() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() V38() V39() V40() V41() V42() set
1 is non empty natural V31() real ext-real positive non negative V36() V37() V38() V39() V40() V41() V46() V47() Element of NAT
{{},1} is non empty set
2 is non empty natural V31() real ext-real positive non negative V36() V37() V38() V39() V40() V41() V46() V47() Element of NAT
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty natural V31() real ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V46() V47() Element of NAT
- 1 is V31() real ext-real non positive Element of REAL
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
{+infty,-infty} is non empty V37() set
REAL \/ {+infty,-infty} is non empty V37() set
{-infty} is non empty V37() set
bool ExtREAL is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of X is non empty set
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
X + fi is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (X + fi) is non empty set
q is set
the carrier of V is non empty set
psi is left_complementable right_complementable complementable Element of the carrier of V
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
psi + (0. V) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,psi,(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is left_complementable right_complementable complementable Element of the carrier of V : ( b₁ in X & b₂ in fi ) } is set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
psi is left_complementable right_complementable complementable Element of the carrier of V
x is left_complementable right_complementable complementable Element of the carrier of V
q is left_complementable right_complementable complementable Element of the carrier of V
psi + x is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[psi,x] is Element of [: the carrier of V, the carrier of V:]
{psi,x} is non empty set
{psi} is non empty set
{{psi,x},{psi}} is non empty set
[psi,x] `1 is left_complementable right_complementable complementable Element of the carrier of V
[psi,x] `2 is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
psi is left_complementable right_complementable complementable Element of the carrier of V
x is left_complementable right_complementable complementable Element of the carrier of V
[psi,x] is Element of [: the carrier of V, the carrier of V:]
{psi,x} is non empty set
{psi} is non empty set
{{psi,x},{psi}} is non empty set
psi + x is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
(q |-- (X,fi)) `1 is left_complementable right_complementable complementable Element of the carrier of V
(q |-- (X,fi)) `2 is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
psi is left_complementable right_complementable complementable Element of the carrier of V
x is left_complementable right_complementable complementable Element of the carrier of V
[psi,x] is Element of [: the carrier of V, the carrier of V:]
{psi,x} is non empty set
{psi} is non empty set
{{psi,x},{psi}} is non empty set
(q |-- (X,fi)) `1 is left_complementable right_complementable complementable Element of the carrier of V
(q |-- (X,fi)) `2 is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
psi is left_complementable right_complementable complementable Element of the carrier of V
x is left_complementable right_complementable complementable Element of the carrier of V
[psi,x] is Element of [: the carrier of V, the carrier of V:]
{psi,x} is non empty set
{psi} is non empty set
{{psi,x},{psi}} is non empty set
q |-- (fi,X) is Element of [: the carrier of V, the carrier of V:]
[x,psi] is Element of [: the carrier of V, the carrier of V:]
{x,psi} is non empty set
{x} is non empty set
{{x,psi},{x}} is non empty set
(q |-- (X,fi)) `1 is left_complementable right_complementable complementable Element of the carrier of V
(q |-- (X,fi)) `2 is left_complementable right_complementable complementable Element of the carrier of V
x + psi is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,x,psi) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[q,(0. V)] is Element of [: the carrier of V, the carrier of V:]
{q,(0. V)} is non empty set
{q} is non empty set
{{q,(0. V)},{q}} is non empty set
q + (0. V) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,q,(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of V
q |-- (X,fi) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[(0. V),q] is Element of [: the carrier of V, the carrier of V:]
{(0. V),q} is non empty set
{(0. V)} is non empty set
{{(0. V),q},{(0. V)}} is non empty set
q |-- (fi,X) is Element of [: the carrier of V, the carrier of V:]
[q,(0. V)] is Element of [: the carrier of V, the carrier of V:]
{q,(0. V)} is non empty set
{q} is non empty set
{{q,(0. V)},{q}} is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of X is non empty set
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of X
q is left_complementable right_complementable complementable Element of the carrier of V
the carrier of fi is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
q is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
X + fi is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of q
x is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of q
psi + x is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of q
the carrier of V is non empty set
the carrier of psi is non empty set
the carrier of q is non empty set
the carrier of x is non empty set
A is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
A is left_complementable right_complementable complementable Element of the carrier of V
psi is left_complementable right_complementable complementable Element of the carrier of q
f is left_complementable right_complementable complementable Element of the carrier of q
Y is left_complementable right_complementable complementable Element of the carrier of q
f + Y is left_complementable right_complementable complementable Element of the carrier of q
the addF of q is Relation-like [: the carrier of q, the carrier of q:] -defined the carrier of q -valued Function-like non empty total V18([: the carrier of q, the carrier of q:], the carrier of q) Element of bool [:[: the carrier of q, the carrier of q:], the carrier of q:]
[: the carrier of q, the carrier of q:] is Relation-like non empty set
[:[: the carrier of q, the carrier of q:], the carrier of q:] is Relation-like non empty set
bool [:[: the carrier of q, the carrier of q:], the carrier of q:] is non empty set
K84( the carrier of q, the addF of q,f,Y) is left_complementable right_complementable complementable Element of the carrier of q
RLSY is left_complementable right_complementable complementable Element of the carrier of V
f9 is left_complementable right_complementable complementable Element of the carrier of V
RLSY + f9 is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,RLSY,f9) is left_complementable right_complementable complementable Element of the carrier of V
psi is left_complementable right_complementable complementable Element of the carrier of V
f is left_complementable right_complementable complementable Element of the carrier of V
psi + f is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,f) is left_complementable right_complementable complementable Element of the carrier of V
Y is left_complementable right_complementable complementable Element of the carrier of q
RLSY is left_complementable right_complementable complementable Element of the carrier of q
Y + RLSY is left_complementable right_complementable complementable Element of the carrier of q
K84( the carrier of q, the addF of q,Y,RLSY) is left_complementable right_complementable complementable Element of the carrier of q
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of X is non empty set
fi is left_complementable right_complementable complementable Element of the carrier of V
{fi} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {fi} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is left_complementable right_complementable complementable Element of the carrier of X
{q} is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of X
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
x is left_complementable right_complementable complementable Element of the carrier of V
A is V31() real ext-real Element of REAL
A * q is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like non empty total V18([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is Relation-like non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K80( the Mult of X,A,q) is set
A * fi is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,A,fi) is set
A is V31() real ext-real Element of REAL
A * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,A,fi) is set
A * q is left_complementable right_complementable complementable Element of the carrier of X
K80( the Mult of X,A,q) is set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
the ZeroF of (fi + (Lin {X})) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the addF of (fi + (Lin {X})) is Relation-like [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
the Mult of (fi + (Lin {X})) is Relation-like [:REAL, the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:REAL, the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
RLSStruct(# the carrier of (fi + (Lin {X})), the ZeroF of (fi + (Lin {X})), the addF of (fi + (Lin {X})), the Mult of (fi + (Lin {X})) #) is non empty strict RLSStruct
psi + (Lin {q}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi /\ (Lin {q}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
(0). (fi + (Lin {X})) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
A is V31() real ext-real Element of REAL
A * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),A,q) is set
0. (fi + (Lin {X})) is V83(fi + (Lin {X})) left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
1 * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),1,q) is set
A " is V31() real ext-real Element of REAL
(A ") * A is V31() real ext-real Element of REAL
((A ") * A) * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),((A ") * A),q) is set
(A ") * (A * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),(A "),(A * q)) is set
0. (fi + (Lin {X})) is V83(fi + (Lin {X})) left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
q |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
the carrier of psi is non empty set
0. psi is V83(psi) left_complementable right_complementable complementable Element of the carrier of psi
the ZeroF of psi is left_complementable right_complementable complementable Element of the carrier of psi
[(0. psi),q] is Element of [: the carrier of psi, the carrier of (fi + (Lin {X})):]
[: the carrier of psi, the carrier of (fi + (Lin {X})):] is Relation-like non empty set
{(0. psi),q} is non empty set
{(0. psi)} is non empty set
{{(0. psi),q},{(0. psi)}} is non empty set
0. (fi + (Lin {X})) is V83(fi + (Lin {X})) left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the ZeroF of (fi + (Lin {X})) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
[(0. (fi + (Lin {X}))),q] is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
{(0. (fi + (Lin {X}))),q} is non empty set
{(0. (fi + (Lin {X})))} is non empty set
{{(0. (fi + (Lin {X}))),q},{(0. (fi + (Lin {X})))}} is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
x |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[x,(0. V)] is Element of [: the carrier of (fi + (Lin {X})), the carrier of V:]
[: the carrier of (fi + (Lin {X})), the carrier of V:] is Relation-like non empty set
{x,(0. V)} is non empty set
{x} is non empty set
{{x,(0. V)},{x}} is non empty set
0. (fi + (Lin {X})) is V83(fi + (Lin {X})) left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the ZeroF of (fi + (Lin {X})) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
[x,(0. (fi + (Lin {X})))] is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
{x,(0. (fi + (Lin {X})))} is non empty set
{{x,(0. (fi + (Lin {X})))},{x}} is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
q is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
X |-- (fi,q) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(X |-- (fi,q)) `1 is left_complementable right_complementable complementable Element of the carrier of V
(X |-- (fi,q)) `2 is left_complementable right_complementable complementable Element of the carrier of V
[((X |-- (fi,q)) `1),((X |-- (fi,q)) `2)] is Element of [: the carrier of V, the carrier of V:]
{((X |-- (fi,q)) `1),((X |-- (fi,q)) `2)} is non empty set
{((X |-- (fi,q)) `1)} is non empty set
{{((X |-- (fi,q)) `1),((X |-- (fi,q)) `2)},{((X |-- (fi,q)) `1)}} is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
the carrier of fi is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
x |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
A is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
A is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
[A,A] is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
{A,A} is non empty set
{A} is non empty set
{{A,A},{A}} is non empty set
f is V31() real ext-real Element of REAL
f * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the Mult of (fi + (Lin {X})) is Relation-like [:REAL, the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:REAL, the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
K80( the Mult of (fi + (Lin {X})),f,q) is set
psi is left_complementable right_complementable complementable Element of the carrier of fi
f * X is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,f,X) is set
[psi,(f * X)] is Element of [: the carrier of fi, the carrier of V:]
[: the carrier of fi, the carrier of V:] is Relation-like non empty set
{psi,(f * X)} is non empty set
{psi} is non empty set
{{psi,(f * X)},{psi}} is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
the carrier of fi is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
x |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
A is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
A |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
x + A is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the addF of (fi + (Lin {X})) is Relation-like [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),x,A) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(x + A) |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
A is left_complementable right_complementable complementable Element of the carrier of fi
psi is left_complementable right_complementable complementable Element of the carrier of fi
A + psi is left_complementable right_complementable complementable Element of the carrier of fi
the addF of fi is Relation-like [: the carrier of fi, the carrier of fi:] -defined the carrier of fi -valued Function-like non empty total V18([: the carrier of fi, the carrier of fi:], the carrier of fi) Element of bool [:[: the carrier of fi, the carrier of fi:], the carrier of fi:]
[: the carrier of fi, the carrier of fi:] is Relation-like non empty set
[:[: the carrier of fi, the carrier of fi:], the carrier of fi:] is Relation-like non empty set
bool [:[: the carrier of fi, the carrier of fi:], the carrier of fi:] is non empty set
K84( the carrier of fi, the addF of fi,A,psi) is left_complementable right_complementable complementable Element of the carrier of fi
f is V31() real ext-real Element of REAL
f * X is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,f,X) is set
[A,(f * X)] is Element of [: the carrier of fi, the carrier of V:]
[: the carrier of fi, the carrier of V:] is Relation-like non empty set
{A,(f * X)} is non empty set
{A} is non empty set
{{A,(f * X)},{A}} is non empty set
Y is V31() real ext-real Element of REAL
Y * X is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,Y,X) is set
[psi,(Y * X)] is Element of [: the carrier of fi, the carrier of V:]
{psi,(Y * X)} is non empty set
{psi} is non empty set
{{psi,(Y * X)},{psi}} is non empty set
f + Y is V31() real ext-real Element of REAL
(f + Y) * X is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(f + Y),X) is set
[(A + psi),((f + Y) * X)] is Element of [: the carrier of fi, the carrier of V:]
{(A + psi),((f + Y) * X)} is non empty set
{(A + psi)} is non empty set
{{(A + psi),((f + Y) * X)},{(A + psi)}} is non empty set
Y * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the Mult of (fi + (Lin {X})) is Relation-like [:REAL, the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:REAL, the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
K80( the Mult of (fi + (Lin {X})),Y,q) is set
f9 is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(f + Y) * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),(f + Y),q) is set
RLSY is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
RLSY + f9 is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),RLSY,f9) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
ggh is left_complementable right_complementable complementable Element of the carrier of V
psi is left_complementable right_complementable complementable Element of the carrier of V
ggh + psi is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,ggh,psi) is left_complementable right_complementable complementable Element of the carrier of V
f * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),f,q) is set
f9 + (Y * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),f9,(Y * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
RLSY + (f * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),RLSY,(f * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(RLSY + (f * q)) + f9 is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(RLSY + (f * q)),f9) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
((RLSY + (f * q)) + f9) + (Y * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),((RLSY + (f * q)) + f9),(Y * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(RLSY + f9) + (f * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(RLSY + f9),(f * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
((RLSY + f9) + (f * q)) + (Y * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),((RLSY + f9) + (f * q)),(Y * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(f * q) + (Y * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(f * q),(Y * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(RLSY + f9) + ((f * q) + (Y * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(RLSY + f9),((f * q) + (Y * q))) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(RLSY + f9) + ((f + Y) * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(RLSY + f9),((f + Y) * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
X is left_complementable right_complementable complementable Element of the carrier of V
{X} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {X} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
fi + (Lin {X}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of V
the carrier of (fi + (Lin {X})) is non empty set
the carrier of fi is non empty set
q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
{q} is non empty Element of bool the carrier of (fi + (Lin {X}))
bool the carrier of (fi + (Lin {X})) is non empty set
Lin {q} is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
psi is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() Subspace of fi + (Lin {X})
x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
x |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] is Relation-like non empty set
A is left_complementable right_complementable complementable Element of the carrier of fi
psi is V31() real ext-real Element of REAL
psi * X is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,psi,X) is set
[A,(psi * X)] is Element of [: the carrier of fi, the carrier of V:]
[: the carrier of fi, the carrier of V:] is Relation-like non empty set
{A,(psi * X)} is non empty set
{A} is non empty set
{{A,(psi * X)},{A}} is non empty set
A is V31() real ext-real Element of REAL
A * x is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the Mult of (fi + (Lin {X})) is Relation-like [:REAL, the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:REAL, the carrier of (fi + (Lin {X})):] is Relation-like non empty set
[:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
K80( the Mult of (fi + (Lin {X})),A,x) is set
(A * x) |-- (psi,(Lin {q})) is Element of [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):]
A * A is left_complementable right_complementable complementable Element of the carrier of fi
the Mult of fi is Relation-like [:REAL, the carrier of fi:] -defined the carrier of fi -valued Function-like non empty total V18([:REAL, the carrier of fi:], the carrier of fi) Element of bool [:[:REAL, the carrier of fi:], the carrier of fi:]
[:REAL, the carrier of fi:] is Relation-like non empty set
[:[:REAL, the carrier of fi:], the carrier of fi:] is Relation-like non empty set
bool [:[:REAL, the carrier of fi:], the carrier of fi:] is non empty set
K80( the Mult of fi,A,A) is set
A * psi is V31() real ext-real Element of REAL
(A * psi) * X is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(A * psi),X) is set
[(A * A),((A * psi) * X)] is Element of [: the carrier of fi, the carrier of V:]
{(A * A),((A * psi) * X)} is non empty set
{(A * A)} is non empty set
{{(A * A),((A * psi) * X)},{(A * A)}} is non empty set
psi * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),psi,q) is set
f is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
f + (psi * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
the addF of (fi + (Lin {X})) is Relation-like [: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):] -defined the carrier of (fi + (Lin {X})) -valued Function-like non empty total V18([: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X}))) Element of bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):]
[:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is Relation-like non empty set
bool [:[: the carrier of (fi + (Lin {X})), the carrier of (fi + (Lin {X})):], the carrier of (fi + (Lin {X})):] is non empty set
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),f,(psi * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
A * (f + (psi * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),A,(f + (psi * q))) is set
A * f is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),A,f) is set
A * (psi * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),A,(psi * q)) is set
(A * f) + (A * (psi * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(A * f),(A * (psi * q))) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
(A * psi) * q is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K80( the Mult of (fi + (Lin {X})),(A * psi),q) is set
(A * f) + ((A * psi) * q) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
K84( the carrier of (fi + (Lin {X})), the addF of (fi + (Lin {X})),(A * f),((A * psi) * q)) is left_complementable right_complementable complementable Element of the carrier of (fi + (Lin {X}))
Y is left_complementable right_complementable complementable Element of the carrier of V
A * Y is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,A,Y) is set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
[: the carrier of V,REAL:] is Relation-like non empty set
bool [: the carrier of V,REAL:] is non empty set
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
[: the carrier of V,REAL:] is Relation-like non empty set
bool [: the carrier of V,REAL:] is non empty set
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
q is left_complementable right_complementable complementable Element of the carrier of V
fi + q is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
K84( the carrier of V, the addF of V,fi,q) is left_complementable right_complementable complementable Element of the carrier of V
X . (fi + q) is V31() real ext-real Element of REAL
X . fi is V31() real ext-real Element of REAL
X . q is V31() real ext-real Element of REAL
(X . fi) + (X . q) is V31() real ext-real Element of REAL
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
X . fi is V31() real ext-real Element of REAL
q is V31() real ext-real Element of REAL
q * fi is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,q,fi) is set
X . (q * fi) is V31() real ext-real Element of REAL
q * (X . fi) is V31() real ext-real Element of REAL
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
X . fi is V31() real ext-real Element of REAL
q is V31() real ext-real Element of REAL
q * fi is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,q,fi) is set
X . (q * fi) is V31() real ext-real Element of REAL
q * (X . fi) is V31() real ext-real Element of REAL
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
X . (0. V) is V31() real ext-real Element of REAL
0 * (0. V) is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,0,(0. V)) is set
X . (0 * (0. V)) is V31() real ext-real Element of REAL
0 * (X . (0. V)) is V31() real ext-real Element of REAL
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
X . fi is V31() real ext-real Element of REAL
q is V31() real ext-real Element of REAL
q * fi is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,q,fi) is set
X . (q * fi) is V31() real ext-real Element of REAL
q * (X . fi) is V31() real ext-real Element of REAL
abs q is V31() real ext-real Element of REAL
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
X . fi is V31() real ext-real Element of REAL
q is V31() real ext-real Element of REAL
q * fi is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
K80( the Mult of V,q,fi) is set
X . (q * fi) is V31() real ext-real Element of REAL
q * (X . fi) is V31() real ext-real Element of REAL
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
X . (0. V) is V31() real ext-real Element of REAL
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of V is non empty set
[: the carrier of V,REAL:] is Relation-like non empty set
bool [: the carrier of V,REAL:] is non empty set
the carrier of V --> 0 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) Element of bool [: the carrier of V,