:: 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,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
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
0 + 0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V31() real ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() Element of REAL
X . fi is V31() real ext-real Element of REAL
(X . fi) + 0 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
fi is left_complementable right_complementable complementable Element of the carrier of V
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
abs q is V31() real ext-real Element of REAL
(abs q) * 0 is V31() real ext-real Element of REAL
X . fi is V31() real ext-real Element of REAL
(abs q) * (X . fi) is V31() real ext-real Element of 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
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
q * 0 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
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) Element of bool [: the carrier of V,REAL:]
fi is left_complementable right_complementable complementable Element of the carrier of V
- fi is left_complementable right_complementable complementable Element of the carrier of V
X . (- fi) is V31() real ext-real Element of REAL
X . fi is V31() real ext-real Element of REAL
- (X . fi) is V31() real ext-real Element of REAL
(- 1) * 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,(- 1),fi) is set
X . ((- 1) * fi) is V31() real ext-real Element of REAL
(- 1) * (X . fi) 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
X is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) (V) (V) 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
- 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 . (- q) is V31() real ext-real Element of REAL
(X . fi) + (X . (- q)) 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
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
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 Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) Element of bool [: the carrier of V,REAL:]
X . (0. V) is V31() real ext-real Element of REAL
(X . (0. V)) + 0 is V31() real ext-real Element of REAL
(0. V) + (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,(0. V),(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
X . ((0. V) + (0. V)) is V31() real ext-real Element of REAL
(X . (0. 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
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
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] is non empty set
fi is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) (X) (X) (X) (X) Element of bool [: the carrier of X,REAL:]
q is left_complementable right_complementable complementable Element of the carrier of V
{q} is non empty Element of bool the carrier of V
bool the carrier of V 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 V
X + (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 V
the carrier of (X + (Lin {q})) is non empty set
[: the carrier of (X + (Lin {q})),REAL:] is Relation-like non empty set
bool [: the carrier of (X + (Lin {q})),REAL:] is non empty set
psi is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
A is V31() real ext-real Element of REAL
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 X + (Lin {q})
{psi} is non empty Element of bool the carrier of (X + (Lin {q}))
bool the carrier of (X + (Lin {q})) is non empty set
Lin {psi} 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 + (Lin {q})
A is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
A |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
[: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):] is Relation-like non empty set
psi is left_complementable right_complementable complementable Element of the carrier of X
f is V31() real ext-real Element of REAL
f * q 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,q) is set
[psi,(f * q)] is Element of [: the carrier of X, the carrier of V:]
[: the carrier of X, the carrier of V:] is Relation-like non empty set
{psi,(f * q)} is non empty set
{psi} is non empty set
{{psi,(f * q)},{psi}} is non empty set
fi . psi is V31() real ext-real Element of REAL
f * A is V31() real ext-real Element of REAL
(fi . psi) + (f * A) is V31() real ext-real Element of REAL
Y is V31() real ext-real Element of REAL
(A |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(A |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
RLSY is left_complementable right_complementable complementable Element of the carrier of X
fi . RLSY is V31() real ext-real Element of REAL
f9 is V31() real ext-real Element of REAL
f9 * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,f9,q) is set
f9 * A is V31() real ext-real Element of REAL
(fi . RLSY) + (f9 * A) 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
A is Relation-like the carrier of (X + (Lin {q})) -defined REAL -valued Function-like non empty total V18( the carrier of (X + (Lin {q})), REAL ) Element of bool [: the carrier of (X + (Lin {q})),REAL:]
psi is set
dom fi is non empty set
f is left_complementable right_complementable complementable Element of the carrier of X
Y is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
Y |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
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
[Y,(0. V)] is Element of [: the carrier of (X + (Lin {q})), the carrier of V:]
[: the carrier of (X + (Lin {q})), the carrier of V:] is Relation-like non empty set
{Y,(0. V)} is non empty set
{Y} is non empty set
{{Y,(0. V)},{Y}} is non empty set
0 * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,0,q) is set
[Y,(0 * q)] is Element of [: the carrier of (X + (Lin {q})), the carrier of V:]
{Y,(0 * q)} is non empty set
{{Y,(0 * q)},{Y}} is non empty set
(Y |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(Y |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
fi . psi is set
fi . f is V31() real ext-real Element of REAL
0 * A is V31() real ext-real Element of REAL
(fi . f) + (0 * A) is V31() real ext-real Element of REAL
A . psi is set
psi |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
the carrier of x is non empty set
0. x is V83(x) left_complementable right_complementable complementable Element of the carrier of x
the ZeroF of x is left_complementable right_complementable complementable Element of the carrier of x
[(0. x),psi] is Element of [: the carrier of x, the carrier of (X + (Lin {q})):]
[: the carrier of x, the carrier of (X + (Lin {q})):] is Relation-like non empty set
{(0. x),psi} is non empty set
{(0. x)} is non empty set
{{(0. x),psi},{(0. x)}} is non empty set
(psi |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
0. X is V83(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
psi is Relation-like the carrier of (X + (Lin {q})) -defined REAL -valued Function-like non empty total V18( the carrier of (X + (Lin {q})), REAL ) Element of bool [: the carrier of (X + (Lin {q})),REAL:]
f is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
Y is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
f + Y is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
the addF of (X + (Lin {q})) is Relation-like [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):] -defined the carrier of (X + (Lin {q})) -valued Function-like non empty total V18([: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q}))) Element of bool [:[: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):]
[:[: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):] is Relation-like non empty set
bool [:[: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):] is non empty set
K84( the carrier of (X + (Lin {q})), the addF of (X + (Lin {q})),f,Y) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
psi . (f + Y) is V31() real ext-real Element of REAL
psi . f is V31() real ext-real Element of REAL
psi . Y is V31() real ext-real Element of REAL
(psi . f) + (psi . Y) is V31() real ext-real Element of REAL
f |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
RLSY is left_complementable right_complementable complementable Element of the carrier of X
f9 is V31() real ext-real Element of REAL
f9 * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,f9,q) is set
[RLSY,(f9 * q)] is Element of [: the carrier of X, the carrier of V:]
{RLSY,(f9 * q)} is non empty set
{RLSY} is non empty set
{{RLSY,(f9 * q)},{RLSY}} is non empty set
(f |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(f |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
Y |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
ggh is left_complementable right_complementable complementable Element of the carrier of X
psi is V31() real ext-real Element of REAL
psi * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,psi,q) is set
[ggh,(psi * q)] is Element of [: the carrier of X, the carrier of V:]
{ggh,(psi * q)} is non empty set
{ggh} is non empty set
{{ggh,(psi * q)},{ggh}} is non empty set
(Y |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(Y |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(f + Y) |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
RLSY + ggh is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K84( the carrier of X, the addF of X,RLSY,ggh) is left_complementable right_complementable complementable Element of the carrier of X
f9 + psi is V31() real ext-real Element of REAL
(f9 + psi) * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(f9 + psi),q) is set
[(RLSY + ggh),((f9 + psi) * q)] is Element of [: the carrier of X, the carrier of V:]
{(RLSY + ggh),((f9 + psi) * q)} is non empty set
{(RLSY + ggh)} is non empty set
{{(RLSY + ggh),((f9 + psi) * q)},{(RLSY + ggh)}} is non empty set
((f + Y) |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
((f + Y) |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
fi . (RLSY + ggh) is V31() real ext-real Element of REAL
(f9 + psi) * A is V31() real ext-real Element of REAL
(fi . (RLSY + ggh)) + ((f9 + psi) * A) is V31() real ext-real Element of REAL
fi . RLSY is V31() real ext-real Element of REAL
fi . ggh is V31() real ext-real Element of REAL
(fi . RLSY) + (fi . ggh) is V31() real ext-real Element of REAL
f9 * A is V31() real ext-real Element of REAL
psi * A is V31() real ext-real Element of REAL
(f9 * A) + (psi * A) is V31() real ext-real Element of REAL
((fi . RLSY) + (fi . ggh)) + ((f9 * A) + (psi * A)) is V31() real ext-real Element of REAL
(fi . RLSY) + (f9 * A) is V31() real ext-real Element of REAL
(fi . ggh) + (psi * A) is V31() real ext-real Element of REAL
((fi . RLSY) + (f9 * A)) + ((fi . ggh) + (psi * A)) is V31() real ext-real Element of REAL
(psi . f) + ((fi . ggh) + (psi * A)) is V31() real ext-real Element of REAL
f is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
psi . f is V31() real ext-real Element of REAL
Y is V31() real ext-real Element of REAL
Y * f is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
the Mult of (X + (Lin {q})) is Relation-like [:REAL, the carrier of (X + (Lin {q})):] -defined the carrier of (X + (Lin {q})) -valued Function-like non empty total V18([:REAL, the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q}))) Element of bool [:[:REAL, the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):]
[:REAL, the carrier of (X + (Lin {q})):] is Relation-like non empty set
[:[:REAL, the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (X + (Lin {q})):], the carrier of (X + (Lin {q})):] is non empty set
K80( the Mult of (X + (Lin {q})),Y,f) is set
psi . (Y * f) is V31() real ext-real Element of REAL
Y * (psi . f) is V31() real ext-real Element of REAL
f |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
RLSY is left_complementable right_complementable complementable Element of the carrier of X
f9 is V31() real ext-real Element of REAL
f9 * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,f9,q) is set
[RLSY,(f9 * q)] is Element of [: the carrier of X, the carrier of V:]
{RLSY,(f9 * q)} is non empty set
{RLSY} is non empty set
{{RLSY,(f9 * q)},{RLSY}} is non empty set
(f |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(f |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
(Y * f) |-- (x,(Lin {psi})) is Element of [: the carrier of (X + (Lin {q})), the carrier of (X + (Lin {q})):]
Y * RLSY 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,Y,RLSY) is set
Y * f9 is V31() real ext-real Element of REAL
(Y * f9) * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(Y * f9),q) is set
[(Y * RLSY),((Y * f9) * q)] is Element of [: the carrier of X, the carrier of V:]
{(Y * RLSY),((Y * f9) * q)} is non empty set
{(Y * RLSY)} is non empty set
{{(Y * RLSY),((Y * f9) * q)},{(Y * RLSY)}} is non empty set
((Y * f) |-- (x,(Lin {psi}))) `1 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
((Y * f) |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
fi . (Y * RLSY) is V31() real ext-real Element of REAL
(Y * f9) * A is V31() real ext-real Element of REAL
(fi . (Y * RLSY)) + ((Y * f9) * A) is V31() real ext-real Element of REAL
fi . RLSY is V31() real ext-real Element of REAL
Y * (fi . RLSY) is V31() real ext-real Element of REAL
f9 * A is V31() real ext-real Element of REAL
Y * (f9 * A) is V31() real ext-real Element of REAL
(Y * (fi . RLSY)) + (Y * (f9 * A)) is V31() real ext-real Element of REAL
(fi . RLSY) + (f9 * A) is V31() real ext-real Element of REAL
Y * ((fi . RLSY) + (f9 * A)) is V31() real ext-real Element of REAL
f is Relation-like the carrier of (X + (Lin {q})) -defined REAL -valued Function-like non empty total V18( the carrier of (X + (Lin {q})), REAL ) (X + (Lin {q})) (X + (Lin {q})) (X + (Lin {q})) (X + (Lin {q})) Element of bool [: the carrier of (X + (Lin {q})),REAL:]
f | the carrier of X is Relation-like the carrier of X -defined the carrier of (X + (Lin {q})) -defined REAL -valued Function-like Element of bool [: the carrier of (X + (Lin {q})),REAL:]
f . psi is V31() real ext-real Element of REAL
dom f is non empty set
(dom f) /\ the carrier of X is set
(psi |-- (x,(Lin {psi}))) `2 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {q}))
1 * q is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,1,q) is set
fi . (0. X) is V31() real ext-real Element of REAL
1 * A is V31() real ext-real Element of REAL
(fi . (0. X)) + (1 * A) is V31() real ext-real Element of REAL
0 + (1 * A) 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
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
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] 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
X + (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
the carrier of (X + (Lin {fi})) is non empty set
[: the carrier of (X + (Lin {fi})),REAL:] is Relation-like non empty set
bool [: the carrier of (X + (Lin {fi})),REAL:] is non empty set
the carrier of (Lin {fi}) is non empty set
(Lin {fi}) + 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 ((Lin {fi}) + X) is non empty set
the left_complementable right_complementable complementable Element of the carrier of X is left_complementable right_complementable complementable Element of the carrier of X
x is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) Element of bool [: the carrier of V,REAL:]
A is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) (X) (X) (X) (X) Element of bool [: the carrier of X,REAL:]
{ ((A . b₁) - (x . (b₂ - fi))) where b₁ is left_complementable right_complementable complementable Element of the carrier of X, b₂ is left_complementable right_complementable complementable Element of the carrier of V : b₁ = b₂ } is set
{ ((A . b₁) + (x . (fi - b₂))) where b₁ is left_complementable right_complementable complementable Element of the carrier of X, b₂ is left_complementable right_complementable complementable Element of the carrier of V : b₁ = b₂ } is set
f is left_complementable right_complementable complementable Element of the carrier of X
RLSY is left_complementable right_complementable complementable Element of the carrier of V
Y is left_complementable right_complementable complementable Element of the carrier of X
f9 is left_complementable right_complementable complementable Element of the carrier of V
f - Y is left_complementable right_complementable complementable Element of the carrier of X
- Y is left_complementable right_complementable complementable Element of the carrier of X
f + (- Y) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K84( the carrier of X, the addF of X,f,(- Y)) is left_complementable right_complementable complementable Element of the carrier of X
A . (f - Y) is V31() real ext-real Element of REAL
RLSY - f9 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
x . (RLSY - f9) is V31() real ext-real Element of REAL
A . f is V31() real ext-real Element of REAL
A . Y is V31() real ext-real Element of REAL
(A . f) - (A . Y) 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
RLSY + (0. V) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,RLSY,(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
(RLSY + (0. V)) + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(RLSY + (0. V)),(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
- fi is left_complementable right_complementable complementable Element of the carrier of V
(- fi) + fi is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(- fi),fi) is left_complementable right_complementable complementable Element of the carrier of V
RLSY + ((- fi) + fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,RLSY,((- fi) + fi)) is left_complementable right_complementable complementable Element of the carrier of V
(RLSY + ((- fi) + fi)) + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(RLSY + ((- fi) + fi)),(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
RLSY - fi is left_complementable right_complementable complementable Element of the carrier of V
RLSY + (- fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,RLSY,(- fi)) is left_complementable right_complementable complementable Element of the carrier of V
(RLSY - fi) + fi is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(RLSY - fi),fi) is left_complementable right_complementable complementable Element of the carrier of V
((RLSY - fi) + fi) + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,((RLSY - fi) + fi),(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
fi - f9 is left_complementable right_complementable complementable Element of the carrier of V
fi + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
(RLSY - fi) + (fi - f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(RLSY - fi),(fi - f9)) is left_complementable right_complementable complementable Element of the carrier of V
x . (RLSY - fi) is V31() real ext-real Element of REAL
x . (fi - f9) is V31() real ext-real Element of REAL
(x . (RLSY - fi)) + (x . (fi - f9)) is V31() real ext-real Element of REAL
(x . (fi - f9)) + (x . (RLSY - fi)) is V31() real ext-real Element of REAL
(A . Y) + ((x . (fi - f9)) + (x . (RLSY - fi))) is V31() real ext-real Element of REAL
(A . Y) + (x . (fi - f9)) is V31() real ext-real Element of REAL
((A . Y) + (x . (fi - f9))) + (x . (RLSY - fi)) is V31() real ext-real Element of REAL
(A . f) - (x . (RLSY - fi)) is V31() real ext-real Element of REAL
f is ext-real Element of ExtREAL
Y is ext-real Element of ExtREAL
RLSY is left_complementable right_complementable complementable Element of the carrier of X
A . RLSY is V31() real ext-real Element of REAL
f9 is left_complementable right_complementable complementable Element of the carrier of V
fi - f9 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
fi + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
x . (fi - f9) is V31() real ext-real Element of REAL
(A . RLSY) + (x . (fi - f9)) is V31() real ext-real Element of REAL
ggh is left_complementable right_complementable complementable Element of the carrier of X
A . ggh is V31() real ext-real Element of REAL
psi is left_complementable right_complementable complementable Element of the carrier of V
psi - fi is left_complementable right_complementable complementable Element of the carrier of V
psi + (- fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,(- fi)) is left_complementable right_complementable complementable Element of the carrier of V
x . (psi - fi) is V31() real ext-real Element of REAL
(A . ggh) - (x . (psi - fi)) is V31() real ext-real Element of REAL
Y is set
RLSY is left_complementable right_complementable complementable Element of the carrier of X
A . RLSY is V31() real ext-real Element of REAL
f9 is left_complementable right_complementable complementable Element of the carrier of V
f9 - fi is left_complementable right_complementable complementable Element of the carrier of V
f9 + (- fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,f9,(- fi)) is left_complementable right_complementable complementable Element of the carrier of V
x . (f9 - fi) is V31() real ext-real Element of REAL
(A . RLSY) - (x . (f9 - fi)) is V31() real ext-real Element of REAL
Y is set
RLSY is left_complementable right_complementable complementable Element of the carrier of X
A . RLSY is V31() real ext-real Element of REAL
f9 is left_complementable right_complementable complementable Element of the carrier of V
fi - f9 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
fi + (- f9) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- f9)) is left_complementable right_complementable complementable Element of the carrier of V
x . (fi - f9) is V31() real ext-real Element of REAL
(A . RLSY) + (x . (fi - f9)) is V31() real ext-real Element of REAL
A . the left_complementable right_complementable complementable Element of the carrier of X is V31() real ext-real Element of REAL
f is left_complementable right_complementable complementable Element of the carrier of V
f - fi is left_complementable right_complementable complementable Element of the carrier of V
f + (- fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,f,(- fi)) is left_complementable right_complementable complementable Element of the carrier of V
x . (f - fi) is V31() real ext-real Element of REAL
(A . the left_complementable right_complementable complementable Element of the carrier of X) - (x . (f - fi)) is V31() real ext-real Element of REAL
fi - f 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
fi + (- f) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- f)) is left_complementable right_complementable complementable Element of the carrier of V
x . (fi - f) is V31() real ext-real Element of REAL
(A . the left_complementable right_complementable complementable Element of the carrier of X) + (x . (fi - f)) is V31() real ext-real Element of REAL
Y is non empty V37() Element of bool ExtREAL
sup Y is ext-real set
RLSY is non empty V37() Element of bool ExtREAL
inf RLSY is ext-real set
the ext-real Element of RLSY is ext-real Element of RLSY
ggh is V31() real ext-real set
psi is ext-real set
-infty is non empty non real ext-real non positive negative Element of ExtREAL
{-infty} is non empty V37() Element of bool ExtREAL
the ext-real Element of Y is ext-real Element of Y
q is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
f9 is V31() real ext-real Element of REAL
ggh is Relation-like the carrier of (X + (Lin {fi})) -defined REAL -valued Function-like non empty total V18( the carrier of (X + (Lin {fi})), REAL ) (X + (Lin {fi})) (X + (Lin {fi})) (X + (Lin {fi})) (X + (Lin {fi})) Element of bool [: the carrier of (X + (Lin {fi})),REAL:]
ggh | the carrier of X is Relation-like the carrier of X -defined the carrier of (X + (Lin {fi})) -defined REAL -valued Function-like Element of bool [: the carrier of (X + (Lin {fi})),REAL:]
ggh . q is V31() real ext-real Element of REAL
psi is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
ggh . psi is V31() real ext-real Element of REAL
x is left_complementable right_complementable complementable Element of the carrier of V
x . x is V31() real ext-real Element of REAL
phi is left_complementable right_complementable complementable Element of the carrier of V
phi is left_complementable right_complementable complementable Element of the carrier of V
phi + phi is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,phi,phi) is left_complementable right_complementable complementable Element of the carrier of V
f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
f9 is V31() real ext-real Element of REAL
f9 * 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,f9,fi) is set
gg is left_complementable right_complementable complementable Element of the carrier of X
A . gg is V31() real ext-real Element of REAL
- f9 is V31() real ext-real Element of REAL
(- f9) " is V31() real ext-real Element of REAL
((- f9) ") * f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
the Mult of (X + (Lin {fi})) is Relation-like [:REAL, the carrier of (X + (Lin {fi})):] -defined the carrier of (X + (Lin {fi})) -valued Function-like non empty total V18([:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi}))) Element of bool [:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):]
[:REAL, the carrier of (X + (Lin {fi})):] is Relation-like non empty set
[:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is non empty set
K80( the Mult of (X + (Lin {fi})),((- f9) "),f9) is set
ggh . (((- f9) ") * f9) is V31() real ext-real Element of REAL
((- f9) ") * phi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,((- f9) "),phi) is set
fi - (((- f9) ") * phi) is left_complementable right_complementable complementable Element of the carrier of V
- (((- f9) ") * phi) is left_complementable right_complementable complementable Element of the carrier of V
fi + (- (((- f9) ") * phi)) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- (((- f9) ") * phi))) is left_complementable right_complementable complementable Element of the carrier of V
x . (fi - (((- f9) ") * phi)) is V31() real ext-real Element of REAL
(ggh . (((- f9) ") * f9)) + (x . (fi - (((- f9) ") * phi))) is V31() real ext-real Element of REAL
f9 " is V31() real ext-real Element of REAL
- (f9 ") is V31() real ext-real Element of REAL
(- (f9 ")) * phi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(- (f9 ")),phi) is set
fi - ((- (f9 ")) * phi) is left_complementable right_complementable complementable Element of the carrier of V
- ((- (f9 ")) * phi) is left_complementable right_complementable complementable Element of the carrier of V
fi + (- ((- (f9 ")) * phi)) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- ((- (f9 ")) * phi))) is left_complementable right_complementable complementable Element of the carrier of V
(f9 ") * phi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(f9 "),phi) is set
- ((f9 ") * phi) is left_complementable right_complementable complementable Element of the carrier of V
- (- ((f9 ") * phi)) is left_complementable right_complementable complementable Element of the carrier of V
fi + (- (- ((f9 ") * phi))) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(- (- ((f9 ") * phi)))) is left_complementable right_complementable complementable Element of the carrier of V
fi + ((f9 ") * phi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,((f9 ") * phi)) is left_complementable right_complementable complementable Element of the carrier of V
gg is left_complementable right_complementable complementable Element of the carrier of X
((- f9) ") * gg 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,((- f9) "),gg) is set
A . (((- f9) ") * gg) is V31() real ext-real Element of REAL
YY is ext-real Element of ExtREAL
f9 - (x . (fi - (((- f9) ") * phi))) is V31() real ext-real Element of REAL
- (ggh . (((- f9) ") * f9)) is V31() real ext-real Element of REAL
- (f9 - (x . (fi - (((- f9) ") * phi)))) is V31() real ext-real Element of REAL
(- 1) * (ggh . (((- f9) ") * f9)) is V31() real ext-real Element of REAL
(- 1) * (((- f9) ") * f9) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),(- 1),(((- f9) ") * f9)) is set
ggh . ((- 1) * (((- f9) ") * f9)) is V31() real ext-real Element of REAL
(- 1) * ((- f9) ") is V31() real ext-real Element of REAL
((- 1) * ((- f9) ")) * f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),((- 1) * ((- f9) ")),f9) is set
ggh . (((- 1) * ((- f9) ")) * f9) is V31() real ext-real Element of REAL
(- 1) * (- (f9 ")) is V31() real ext-real Element of REAL
((- 1) * (- (f9 "))) * f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),((- 1) * (- (f9 "))),f9) is set
ggh . (((- 1) * (- (f9 "))) * f9) is V31() real ext-real Element of REAL
(f9 ") * f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),(f9 "),f9) is set
ggh . ((f9 ") * f9) is V31() real ext-real Element of REAL
x . (fi + ((f9 ") * phi)) is V31() real ext-real Element of REAL
(x . (fi + ((f9 ") * phi))) - f9 is V31() real ext-real Element of REAL
(f9 ") * x is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(f9 "),x) is set
(f9 ") * phi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(f9 "),phi) is set
((f9 ") * phi) + ((f9 ") * phi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,((f9 ") * phi),((f9 ") * phi)) is left_complementable right_complementable complementable Element of the carrier of V
(f9 ") * f9 is V31() real ext-real Element of REAL
((f9 ") * f9) * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,((f9 ") * f9),fi) is set
((f9 ") * phi) + (((f9 ") * f9) * fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,((f9 ") * phi),(((f9 ") * f9) * fi)) is left_complementable right_complementable complementable Element of the carrier of V
1 * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,1,fi) is set
((f9 ") * phi) + (1 * fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,((f9 ") * phi),(1 * fi)) is left_complementable right_complementable complementable Element of the carrier of V
(ggh . ((f9 ") * f9)) + f9 is V31() real ext-real Element of REAL
x . ((f9 ") * x) is V31() real ext-real Element of REAL
(f9 ") * (x . x) is V31() real ext-real Element of REAL
ff is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
f9 * q is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),f9,q) is set
f9 + (f9 * q) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
the addF of (X + (Lin {fi})) is Relation-like [: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):] -defined the carrier of (X + (Lin {fi})) -valued Function-like non empty total V18([: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi}))) Element of bool [:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):]
[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):] is Relation-like non empty set
[:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is Relation-like non empty set
bool [:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is non empty set
K84( the carrier of (X + (Lin {fi})), the addF of (X + (Lin {fi})),f9,(f9 * q)) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
f9 * ((f9 ") * (x . x)) is V31() real ext-real Element of REAL
f9 * (f9 ") is V31() real ext-real Element of REAL
(f9 * (f9 ")) * (x . x) is V31() real ext-real Element of REAL
1 * (x . x) is V31() real ext-real Element of REAL
ggh . (f9 + (f9 * q)) is V31() real ext-real Element of REAL
ggh . f9 is V31() real ext-real Element of REAL
ggh . (f9 * q) is V31() real ext-real Element of REAL
(ggh . f9) + (ggh . (f9 * q)) is V31() real ext-real Element of REAL
f9 * (ggh . q) is V31() real ext-real Element of REAL
(ggh . f9) + (f9 * (ggh . q)) is V31() real ext-real Element of REAL
1 * ((ggh . f9) + (f9 * (ggh . q))) is V31() real ext-real Element of REAL
(f9 * (f9 ")) * ((ggh . f9) + (f9 * (ggh . q))) is V31() real ext-real Element of REAL
(f9 ") * (ggh . f9) is V31() real ext-real Element of REAL
((f9 ") * f9) * (ggh . q) is V31() real ext-real Element of REAL
((f9 ") * (ggh . f9)) + (((f9 ") * f9) * (ggh . q)) is V31() real ext-real Element of REAL
f9 * (((f9 ") * (ggh . f9)) + (((f9 ") * f9) * (ggh . q))) is V31() real ext-real Element of REAL
1 * (ggh . q) is V31() real ext-real Element of REAL
((f9 ") * (ggh . f9)) + (1 * (ggh . q)) is V31() real ext-real Element of REAL
f9 * (((f9 ") * (ggh . f9)) + (1 * (ggh . q))) is V31() real ext-real Element of REAL
f9 * ((ggh . ((f9 ") * f9)) + f9) is V31() real ext-real Element of REAL
- phi is left_complementable right_complementable complementable Element of the carrier of V
- f9 is V31() real ext-real Element of REAL
(- f9) " is V31() real ext-real Element of REAL
((- f9) ") * f9 is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
the Mult of (X + (Lin {fi})) is Relation-like [:REAL, the carrier of (X + (Lin {fi})):] -defined the carrier of (X + (Lin {fi})) -valued Function-like non empty total V18([:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi}))) Element of bool [:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):]
[:REAL, the carrier of (X + (Lin {fi})):] is Relation-like non empty set
[:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is Relation-like non empty set
bool [:[:REAL, the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is non empty set
K80( the Mult of (X + (Lin {fi})),((- f9) "),f9) is set
ggh . (((- f9) ") * f9) is V31() real ext-real Element of REAL
((- f9) ") * phi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,((- f9) "),phi) is set
(((- f9) ") * phi) - fi is left_complementable right_complementable complementable Element of the carrier of V
(((- f9) ") * phi) + (- fi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(((- f9) ") * phi),(- fi)) is left_complementable right_complementable complementable Element of the carrier of V
x . ((((- f9) ") * phi) - fi) is V31() real ext-real Element of REAL
(ggh . (((- f9) ") * f9)) - (x . ((((- f9) ") * phi) - fi)) is V31() real ext-real Element of REAL
phi - (- phi) is left_complementable right_complementable complementable Element of the carrier of V
- (- phi) is left_complementable right_complementable complementable Element of the carrier of V
phi + (- (- phi)) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,phi,(- (- phi))) is left_complementable right_complementable complementable Element of the carrier of V
(- f9) * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(- f9),fi) is set
YY is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
(- f9) * q is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
K80( the Mult of (X + (Lin {fi})),(- f9),q) is set
f9 - ((- f9) * q) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
- ((- f9) * q) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
f9 + (- ((- f9) * q)) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
the addF of (X + (Lin {fi})) is Relation-like [: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):] -defined the carrier of (X + (Lin {fi})) -valued Function-like non empty total V18([: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi}))) Element of bool [:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):]
[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):] is Relation-like non empty set
[:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is Relation-like non empty set
bool [:[: the carrier of (X + (Lin {fi})), the carrier of (X + (Lin {fi})):], the carrier of (X + (Lin {fi})):] is non empty set
K84( the carrier of (X + (Lin {fi})), the addF of (X + (Lin {fi})),f9,(- ((- f9) * q))) is left_complementable right_complementable complementable Element of the carrier of (X + (Lin {fi}))
gg is left_complementable right_complementable complementable Element of the carrier of X
((- f9) ") * gg 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,((- f9) "),gg) is set
A . (((- f9) ") * gg) is V31() real ext-real Element of REAL
ff is ext-real Element of ExtREAL
f9 + (x . ((((- f9) ") * phi) - fi)) is V31() real ext-real Element of REAL
((- f9) ") * x is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,((- f9) "),x) is set
((- f9) ") * (- phi) is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,((- f9) "),(- phi)) is set
(((- f9) ") * phi) - (((- f9) ") * (- phi)) is left_complementable right_complementable complementable Element of the carrier of V
- (((- f9) ") * (- phi)) is left_complementable right_complementable complementable Element of the carrier of V
(((- f9) ") * phi) + (- (((- f9) ") * (- phi))) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(((- f9) ") * phi),(- (((- f9) ") * (- phi)))) is left_complementable right_complementable complementable Element of the carrier of V
((- f9) ") * (- f9) is V31() real ext-real Element of REAL
(((- f9) ") * (- f9)) * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(((- f9) ") * (- f9)),fi) is set
(((- f9) ") * phi) - ((((- f9) ") * (- f9)) * fi) is left_complementable right_complementable complementable Element of the carrier of V
- ((((- f9) ") * (- f9)) * fi) is left_complementable right_complementable complementable Element of the carrier of V
(((- f9) ") * phi) + (- ((((- f9) ") * (- f9)) * fi)) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(((- f9) ") * phi),(- ((((- f9) ") * (- f9)) * fi))) is left_complementable right_complementable complementable Element of the carrier of V
1 * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,1,fi) is set
(((- f9) ") * phi) - (1 * fi) is left_complementable right_complementable complementable Element of the carrier of V
- (1 * fi) is left_complementable right_complementable complementable Element of the carrier of V
(((- f9) ") * phi) + (- (1 * fi)) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(((- f9) ") * phi),(- (1 * fi))) is left_complementable right_complementable complementable Element of the carrier of V
(ggh . (((- f9) ") * f9)) - f9 is V31() real ext-real Element of REAL
x . (((- f9) ") * x) is V31() real ext-real Element of REAL
((- f9) ") * (x . x) is V31() real ext-real Element of REAL
(- f9) * (((- f9) ") * (x . x)) is V31() real ext-real Element of REAL
(- f9) * ((- f9) ") is V31() real ext-real Element of REAL
((- f9) * ((- f9) ")) * (x . x) is V31() real ext-real Element of REAL
1 * (x . x) is V31() real ext-real Element of REAL
ggh . (f9 - ((- f9) * q)) is V31() real ext-real Element of REAL
ggh . f9 is V31() real ext-real Element of REAL
ggh . ((- f9) * q) is V31() real ext-real Element of REAL
(ggh . f9) - (ggh . ((- f9) * q)) is V31() real ext-real Element of REAL
(- f9) * (ggh . q) is V31() real ext-real Element of REAL
(ggh . f9) - ((- f9) * (ggh . q)) is V31() real ext-real Element of REAL
1 * ((ggh . f9) - ((- f9) * (ggh . q))) is V31() real ext-real Element of REAL
((- f9) * ((- f9) ")) * ((ggh . f9) - ((- f9) * (ggh . q))) is V31() real ext-real Element of REAL
((- f9) ") * (ggh . f9) is V31() real ext-real Element of REAL
(((- f9) ") * (- f9)) * (ggh . q) is V31() real ext-real Element of REAL
(((- f9) ") * (ggh . f9)) - ((((- f9) ") * (- f9)) * (ggh . q)) is V31() real ext-real Element of REAL
(- f9) * ((((- f9) ") * (ggh . f9)) - ((((- f9) ") * (- f9)) * (ggh . q))) is V31() real ext-real Element of REAL
1 * (ggh . q) is V31() real ext-real Element of REAL
(((- f9) ") * (ggh . f9)) - (1 * (ggh . q)) is V31() real ext-real Element of REAL
(- f9) * ((((- f9) ") * (ggh . f9)) - (1 * (ggh . q))) is V31() real ext-real Element of REAL
(- f9) * ((ggh . (((- f9) ") * f9)) - f9) 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 ZeroF of 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
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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty set
q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is left_complementable right_complementable complementable Element of the carrier of V
psi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi is left_complementable right_complementable complementable Element of the carrier of V
q + psi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Relation-like [: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] -defined the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) -valued Function-like non empty total V18([: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) Element of bool [:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):]
[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is non empty set
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),q,psi) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + fi is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,X,fi) is left_complementable right_complementable complementable Element of the carrier of V
x is V31() real ext-real Element of REAL
x * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Relation-like [:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] -defined the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) -valued Function-like non empty total V18([:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) Element of bool [:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):]
[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
[:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
bool [:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is non empty set
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),x,q) is set
x * X is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,x,X) is set
X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Relation-like [: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] -defined the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) -valued Function-like non empty total V18([: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) Element of bool [:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):]
[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is non empty set
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,fi) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
psi 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 + q is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,q) is left_complementable right_complementable complementable Element of the carrier of V
fi + X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),fi,X) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,fi) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
(X + fi) + q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),(X + fi),q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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
psi + x is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
A is left_complementable right_complementable complementable Element of the carrier of V
(psi + x) + A is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(psi + x),A) is left_complementable right_complementable complementable Element of the carrier of V
x + A is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,x,A) is left_complementable right_complementable complementable Element of the carrier of V
psi + (x + A) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,(x + A)) is left_complementable right_complementable complementable Element of the carrier of V
fi + q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),fi,q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + (fi + q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,(fi + q)) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is V83( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the ZeroF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,(0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #))) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi 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
fi + (0. V) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,fi,(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
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
K84( the carrier of V, the addF of V,fi,q) is left_complementable right_complementable complementable Element of the carrier of V
psi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X + psi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,psi) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
fi + q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),fi,q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is V31() real ext-real set
X * (fi + q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Relation-like [:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] -defined the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) -valued Function-like non empty total V18([:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) Element of bool [:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):]
[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
[:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is Relation-like non empty set
bool [:[:REAL, the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):], the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #):] is non empty set
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,(fi + q)) is 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 left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
X * (psi + x) is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,X,(psi + x)) is set
X * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,X,psi) is set
X * x is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,X,x) is set
(X * psi) + (X * x) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(X * psi),(X * x)) is left_complementable right_complementable complementable Element of the carrier of V
X * fi is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,fi) is set
X * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,q) is set
(X * fi) + (X * q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),(X * fi),(X * q)) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is V31() real ext-real set
fi is V31() real ext-real set
X + fi is V31() real ext-real set
(X + fi) * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),(X + fi),q) is set
psi is left_complementable right_complementable complementable Element of the carrier of V
(X + fi) * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(X + fi),psi) is set
X * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,X,psi) is set
fi * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,fi,psi) is set
(X * psi) + (fi * psi) is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,(X * psi),(fi * psi)) is left_complementable right_complementable complementable Element of the carrier of V
X * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,q) is set
fi * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),fi,q) is set
(X * q) + (fi * q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K84( the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #), the addF of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),(X * q),(fi * q)) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
X is V31() real ext-real set
fi is V31() real ext-real set
X * fi is V31() real ext-real set
(X * fi) * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),(X * fi),q) is set
psi is left_complementable right_complementable complementable Element of the carrier of V
(X * fi) * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,(X * fi),psi) is set
fi * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,fi,psi) is set
X * (fi * psi) is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,X,(fi * psi)) is set
fi * q is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),fi,q) is set
X * (fi * q) is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),X,(fi * q)) is set
X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
1 * X is Element of the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
K80( the Mult of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #),1,X) is set
fi is left_complementable right_complementable complementable Element of the carrier of V
1 * fi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,1,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
the ZeroF of 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
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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
fi 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
the carrier of q is non empty set
the ZeroF of q 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
the Mult of q is Relation-like [:REAL, the carrier of q:] -defined the carrier of q -valued Function-like non empty total V18([:REAL, the carrier of q:], the carrier of q) Element of bool [:[:REAL, the carrier of q:], the carrier of q:]
[:REAL, the carrier of q:] is Relation-like non empty set
[:[:REAL, the carrier of q:], the carrier of q:] is Relation-like non empty set
bool [:[:REAL, the carrier of q:], the carrier of q:] is non empty set
RLSStruct(# the carrier of q, the ZeroF of q, the addF of q, the Mult of q #) is non empty strict RLSStruct
the carrier of fi is non empty set
the carrier of X is non empty set
0. fi is V83(fi) left_complementable right_complementable complementable Element of the carrier of fi
the ZeroF of fi is left_complementable right_complementable complementable Element of the carrier of fi
0. X is V83(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
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
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X || the carrier of fi is set
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
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
the Mult of X | [:REAL, the carrier of fi:] is Relation-like [:REAL, the carrier of fi:] -defined [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like set
0. q is V83(q) left_complementable right_complementable complementable Element of the carrier of q
0. V is V83(V) left_complementable right_complementable complementable Element of the carrier of V
the Mult of X | [:REAL, the carrier of fi:] is Relation-like [:REAL, the carrier of fi:] -defined [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of 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
the ZeroF of 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
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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
[: the carrier of V,REAL:] is Relation-like non empty set
bool [: the carrier of V,REAL:] 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() RLSStruct
the carrier of X is non empty set
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] is non empty set
fi is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) (X) (X) (X) (X) Element of bool [: the carrier of X,REAL:]
q 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:]
psi is left_complementable right_complementable complementable Element of the carrier of V
q . psi is V31() real ext-real Element of REAL
x is V31() real ext-real Element of REAL
x * psi is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,x,psi) is set
q . (x * psi) is V31() real ext-real Element of REAL
x * (q . psi) is V31() real ext-real Element of REAL
A is left_complementable right_complementable complementable Element of the carrier of X
x * A 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,x,A) is set
q . (x * A) is 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 left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
q . (psi + x) is V31() real ext-real Element of REAL
q . psi is V31() real ext-real Element of REAL
q . x is V31() real ext-real Element of REAL
(q . psi) + (q . x) is V31() real ext-real Element of REAL
A is left_complementable right_complementable complementable Element of the carrier of X
A is left_complementable right_complementable complementable Element of the carrier of X
A + A is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K84( the carrier of X, the addF of X,A,A) is left_complementable right_complementable complementable Element of the carrier of X
fi . (A + A) 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 ZeroF of 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
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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
[: the carrier of V,REAL:] is Relation-like non empty set
bool [: the carrier of V,REAL:] 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() RLSStruct
the carrier of X is non empty set
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] is non empty set
fi is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) (V) (V) Element of bool [: the carrier of V,REAL:]
q is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
psi is left_complementable right_complementable complementable Element of the carrier of X
q . psi is V31() real ext-real Element of REAL
x is V31() real ext-real Element of REAL
x * psi 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,x,psi) is set
q . (x * psi) is V31() real ext-real Element of REAL
x * (q . psi) is V31() real ext-real Element of REAL
A is left_complementable right_complementable complementable Element of the carrier of V
x * A is left_complementable right_complementable complementable Element of the carrier of V
K80( the Mult of V,x,A) is set
q . (x * A) is set
psi is left_complementable right_complementable complementable Element of the carrier of X
x is left_complementable right_complementable complementable Element of the carrier of X
psi + x is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K84( the carrier of X, the addF of X,psi,x) is left_complementable right_complementable complementable Element of the carrier of X
q . (psi + x) is V31() real ext-real Element of REAL
q . psi is V31() real ext-real Element of REAL
q . x is V31() real ext-real Element of REAL
(q . psi) + (q . x) is V31() real ext-real Element of REAL
A is left_complementable right_complementable complementable Element of the carrier of V
A is left_complementable right_complementable complementable Element of the carrier of V
A + A is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,A,A) is left_complementable right_complementable complementable Element of the carrier of V
fi . (A + A) 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
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
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] is non empty set
fi is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) Element of bool [: the carrier of V,REAL:]
q is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) (X) (X) (X) (X) Element of bool [: the carrier of X,REAL:]
PFuncs ( the carrier of X,REAL) is functional non empty set
PFuncs ( the carrier of V,REAL) is functional non empty set
the ZeroF of 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
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
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
bool (PFuncs ( the carrier of V,REAL)) is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL) : S₁[b₁] } is set
psi is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL)
psi | the carrier of X is Relation-like Function-like set
A is functional Element of bool (PFuncs ( the carrier of V,REAL))
A is functional non empty Element of bool (PFuncs ( the carrier of V,REAL))
psi is Relation-like Function-like Element of A
f is Relation-like Function-like Element of A
psi is Relation-like Function-like Element of A
f is Relation-like Function-like Element of A
Y is Relation-like Function-like Element of A
psi is set
the Relation-like Function-like Element of A is Relation-like Function-like Element of A
RLSY is Relation-like Function-like Element of A
Y is Relation-like Function-like Element of A
f is set
Y is set
union psi is set
the Element of psi is Element of psi
Y is functional non empty set
{ (dom b₁) where b₁ is Relation-like Function-like Element of Y : verum } is set
f is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL)
dom f is set
union { (dom b₁) where b₁ is Relation-like Function-like Element of Y : verum } is set
ggh is set
psi is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL)
psi | the carrier of X is Relation-like Function-like 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
[: the carrier of x,REAL:] is Relation-like non empty set
bool [: the carrier of x,REAL:] is non empty set
phi is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) (x) (x) (x) (x) Element of bool [: the carrier of x,REAL:]
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
[: the carrier of x,REAL:] is Relation-like non empty set
bool [: the carrier of x,REAL:] is non empty set
phi 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 phi is non empty set
[: the carrier of phi,REAL:] is Relation-like non empty set
bool [: the carrier of phi,REAL:] is non empty set
phi is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) (x) (x) (x) (x) Element of bool [: the carrier of x,REAL:]
phi is Relation-like the carrier of phi -defined REAL -valued Function-like non empty total V18( the carrier of phi, REAL ) (phi) (phi) (phi) (phi) Element of bool [: the carrier of phi,REAL:]
f9 is Relation-like the carrier of phi -defined REAL -valued Function-like non empty total V18( the carrier of phi, REAL ) (phi) (phi) (phi) (phi) Element of bool [: the carrier of phi,REAL:]
gg is Relation-like the carrier of phi -defined REAL -valued Function-like non empty total V18( the carrier of phi, REAL ) (phi) (phi) (phi) (phi) Element of bool [: the carrier of phi,REAL:]
gg | the carrier of X is Relation-like the carrier of X -defined the carrier of phi -defined REAL -valued Function-like Element of bool [: the carrier of phi,REAL:]
f9 is left_complementable right_complementable complementable Element of the carrier of phi
YY is left_complementable right_complementable complementable Element of the carrier of V
gg . f9 is V31() real ext-real Element of REAL
fi . YY is V31() real ext-real Element of REAL
ggh is set
psi is Relation-like Function-like Element of Y
dom psi is 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
[: the carrier of x,REAL:] is Relation-like non empty set
bool [: the carrier of x,REAL:] is non empty set
phi is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) (x) (x) (x) (x) Element of bool [: the carrier of x,REAL:]
phi | the carrier of X is Relation-like the carrier of X -defined the carrier of x -defined REAL -valued Function-like Element of bool [: the carrier of x,REAL:]
ggh 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 ggh is non empty set
[: the carrier of ggh,REAL:] is Relation-like non empty set
bool [: the carrier of ggh,REAL:] is non empty set
psi is Relation-like the carrier of ggh -defined REAL -valued Function-like non empty total V18( the carrier of ggh, REAL ) (ggh) (ggh) (ggh) (ggh) Element of bool [: the carrier of ggh,REAL:]
psi | the carrier of X is Relation-like the carrier of X -defined the carrier of ggh -defined REAL -valued Function-like Element of bool [: the carrier of ggh,REAL:]
bool the carrier of V is non empty set
ggh is non empty Element of bool the carrier 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
phi is set
phi is Relation-like Function-like Element of Y
dom phi is set
f9 is set
gg is Relation-like Function-like Element of Y
dom gg is set
f9 is Relation-like Function-like Element of Y
YY 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 YY is non empty set
[: the carrier of YY,REAL:] is Relation-like non empty set
bool [: the carrier of YY,REAL:] is non empty set
ff is Relation-like the carrier of YY -defined REAL -valued Function-like non empty total V18( the carrier of YY, REAL ) (YY) (YY) (YY) (YY) Element of bool [: the carrier of YY,REAL:]
ff | the carrier of X is Relation-like the carrier of X -defined the carrier of YY -defined REAL -valued Function-like Element of bool [: the carrier of YY,REAL:]
dom f9 is set
psi + x is left_complementable right_complementable complementable Element of the carrier of V
K84( the carrier of V, the addF of V,psi,x) is left_complementable right_complementable complementable Element of the carrier of V
psi is V31() real ext-real Element of REAL
x 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
K80( the Mult of V,psi,x) is set
phi is set
phi is Relation-like Function-like Element of Y
dom phi is set
f9 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 f9 is non empty set
[: the carrier of f9,REAL:] is Relation-like non empty set
bool [: the carrier of f9,REAL:] is non empty set
gg is Relation-like the carrier of f9 -defined REAL -valued Function-like non empty total V18( the carrier of f9, REAL ) (f9) (f9) (f9) (f9) Element of bool [: the carrier of f9,REAL:]
gg | the carrier of X is Relation-like the carrier of X -defined the carrier of f9 -defined REAL -valued Function-like Element of bool [: the carrier of f9,REAL:]
psi 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 psi is non empty set
the Element of dom f is Element of dom f
phi is set
[: the carrier of psi,REAL:] is Relation-like non empty set
bool [: the carrier of psi,REAL:] is non empty set
f9 is Relation-like Function-like set
dom f9 is set
rng f9 is set
phi is Relation-like the carrier of psi -defined REAL -valued Function-like non empty total V18( the carrier of psi, REAL ) Element of bool [: the carrier of psi,REAL:]
gg is Relation-like Function-like Element of Y
dom gg is set
f9 is Relation-like the carrier of psi -defined REAL -valued Function-like non empty total V18( the carrier of psi, REAL ) Element of bool [: the carrier of psi,REAL:]
f9 is left_complementable right_complementable complementable Element of the carrier of psi
YY is left_complementable right_complementable complementable Element of the carrier of psi
f9 + YY is left_complementable right_complementable complementable Element of the carrier of psi
the addF of psi is Relation-like [: the carrier of psi, the carrier of psi:] -defined the carrier of psi -valued Function-like non empty total V18([: the carrier of psi, the carrier of psi:], the carrier of psi) Element of bool [:[: the carrier of psi, the carrier of psi:], the carrier of psi:]
[: the carrier of psi, the carrier of psi:] is Relation-like non empty set
[:[: the carrier of psi, the carrier of psi:], the carrier of psi:] is Relation-like non empty set
bool [:[: the carrier of psi, the carrier of psi:], the carrier of psi:] is non empty set
K84( the carrier of psi, the addF of psi,f9,YY) is left_complementable right_complementable complementable Element of the carrier of psi
f9 . (f9 + YY) is V31() real ext-real Element of REAL
f9 . f9 is V31() real ext-real Element of REAL
f9 . YY is V31() real ext-real Element of REAL
(f9 . f9) + (f9 . YY) is V31() real ext-real Element of REAL
ff is set
u is Relation-like Function-like Element of Y
dom u is set
u is set
x is Relation-like Function-like Element of Y
dom x is set
ff is Relation-like Function-like Element of Y
y9 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 y9 is non empty set
[: the carrier of y9,REAL:] is Relation-like non empty set
bool [: the carrier of y9,REAL:] is non empty set
ff is Relation-like the carrier of y9 -defined REAL -valued Function-like non empty total V18( the carrier of y9, REAL ) (y9) (y9) (y9) (y9) Element of bool [: the carrier of y9,REAL:]
ff | the carrier of X is Relation-like the carrier of X -defined the carrier of y9 -defined REAL -valued Function-like Element of bool [: the carrier of y9,REAL:]
dom ff is set
dom ff is non empty set
x9 is left_complementable right_complementable complementable Element of the carrier of y9
y9 is left_complementable right_complementable complementable Element of the carrier of y9
x9 + y9 is left_complementable right_complementable complementable Element of the carrier of y9
the addF of y9 is Relation-like [: the carrier of y9, the carrier of y9:] -defined the carrier of y9 -valued Function-like non empty total V18([: the carrier of y9, the carrier of y9:], the carrier of y9) Element of bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:]
[: the carrier of y9, the carrier of y9:] is Relation-like non empty set
[:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is Relation-like non empty set
bool [:[: the carrier of y9, the carrier of y9:], the carrier of y9:] is non empty set
K84( the carrier of y9, the addF of y9,x9,y9) is left_complementable right_complementable complementable Element of the carrier of y9
ff . (x9 + y9) is V31() real ext-real Element of REAL
ff . x9 is V31() real ext-real Element of REAL
ff . y9 is V31() real ext-real Element of REAL
(ff . x9) + (ff . y9) is V31() real ext-real Element of REAL
(f9 . f9) + (ff . y9) is V31() real ext-real Element of REAL
f9 is left_complementable right_complementable complementable Element of the carrier of psi
f9 . f9 is V31() real ext-real Element of REAL
YY is V31() real ext-real Element of REAL
YY * f9 is left_complementable right_complementable complementable Element of the carrier of psi
the Mult of psi is Relation-like [:REAL, the carrier of psi:] -defined the carrier of psi -valued Function-like non empty total V18([:REAL, the carrier of psi:], the carrier of psi) Element of bool [:[:REAL, the carrier of psi:], the carrier of psi:]
[:REAL, the carrier of psi:] is Relation-like non empty set
[:[:REAL, the carrier of psi:], the carrier of psi:] is Relation-like non empty set
bool [:[:REAL, the carrier of psi:], the carrier of psi:] is non empty set
K80( the Mult of psi,YY,f9) is set
f9 . (YY * f9) is V31() real ext-real Element of REAL
YY * (f9 . f9) is V31() real ext-real Element of REAL
ff is set
u is Relation-like Function-like Element of Y
dom u is set
u 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 u is non empty set
[: the carrier of u,REAL:] is Relation-like non empty set
bool [: the carrier of u,REAL:] is non empty set
x is Relation-like the carrier of u -defined REAL -valued Function-like non empty total V18( the carrier of u, REAL ) (u) (u) (u) (u) Element of bool [: the carrier of u,REAL:]
x | the carrier of X is Relation-like the carrier of X -defined the carrier of u -defined REAL -valued Function-like Element of bool [: the carrier of u,REAL:]
dom x is non empty set
ff is left_complementable right_complementable complementable Element of the carrier of u
YY * ff is left_complementable right_complementable complementable Element of the carrier of u
the Mult of u is Relation-like [:REAL, the carrier of u:] -defined the carrier of u -valued Function-like non empty total V18([:REAL, the carrier of u:], the carrier of u) Element of bool [:[:REAL, the carrier of u:], the carrier of u:]
[:REAL, the carrier of u:] is Relation-like non empty set
[:[:REAL, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[:REAL, the carrier of u:], the carrier of u:] is non empty set
K80( the Mult of u,YY,ff) is set
x . (YY * ff) is V31() real ext-real Element of REAL
x . ff is V31() real ext-real Element of REAL
YY * (x . ff) is V31() real ext-real Element of REAL
YY is left_complementable right_complementable complementable Element of the carrier of psi
ff is left_complementable right_complementable complementable Element of the carrier of V
u is set
u is Relation-like Function-like Element of Y
dom u is 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
[: the carrier of x,REAL:] is Relation-like non empty set
bool [: the carrier of x,REAL:] is non empty set
ff is Relation-like the carrier of x -defined REAL -valued Function-like non empty total V18( the carrier of x, REAL ) (x) (x) (x) (x) Element of bool [: the carrier of x,REAL:]
ff | the carrier of X is Relation-like the carrier of X -defined the carrier of x -defined REAL -valued Function-like Element of bool [: the carrier of x,REAL:]
dom ff is non empty set
f9 is Relation-like the carrier of psi -defined REAL -valued Function-like non empty total V18( the carrier of psi, REAL ) (psi) (psi) (psi) (psi) Element of bool [: the carrier of psi,REAL:]
y9 is left_complementable right_complementable complementable Element of the carrier of x
ff . y9 is V31() real ext-real Element of REAL
fi . ff is V31() real ext-real Element of REAL
f9 . YY is V31() real ext-real Element of REAL
YY 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 YY is non empty set
[: the carrier of YY,REAL:] is Relation-like non empty set
bool [: the carrier of YY,REAL:] is non empty set
ff is Relation-like the carrier of YY -defined REAL -valued Function-like non empty total V18( the carrier of YY, REAL ) (YY) (YY) (YY) (YY) Element of bool [: the carrier of YY,REAL:]
ff | the carrier of X is Relation-like the carrier of X -defined the carrier of YY -defined REAL -valued Function-like Element of bool [: the carrier of YY,REAL:]
dom ff is non empty set
f | the carrier of X is Relation-like Function-like set
u is Relation-like Function-like Element of A
x is Relation-like Function-like Element of A
u is Relation-like Function-like Element of A
psi is Relation-like Function-like Element of A
psi is Relation-like Function-like Element of A
f is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL)
f | the carrier of X is Relation-like Function-like set
Y 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 Y is non empty set
[: the carrier of Y,REAL:] is Relation-like non empty set
bool [: the carrier of Y,REAL:] is non empty set
RLSY is Relation-like the carrier of Y -defined REAL -valued Function-like non empty total V18( the carrier of Y, REAL ) (Y) (Y) (Y) (Y) Element of bool [: the carrier of Y,REAL:]
Y 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 Y is non empty set
[: the carrier of Y,REAL:] is Relation-like non empty set
bool [: the carrier of Y,REAL:] is non empty set
the ZeroF of Y is left_complementable right_complementable complementable Element of the carrier of Y
the addF of Y is Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like non empty total 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 Relation-like non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is Relation-like non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y is Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like non empty total V18([:REAL, the carrier of Y:], the carrier of Y) Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is Relation-like non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is Relation-like non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
RLSStruct(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y #) is non empty strict RLSStruct
f9 is Relation-like the carrier of Y -defined REAL -valued Function-like non empty total V18( the carrier of Y, REAL ) (Y) (Y) (Y) (Y) Element of bool [: the carrier of Y,REAL:]
f9 is Relation-like the carrier of Y -defined REAL -valued Function-like non empty total V18( the carrier of Y, REAL ) (Y) (Y) (Y) (Y) Element of bool [: the carrier of Y,REAL:]
RLSY 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() RLSStruct
ggh is set
psi is left_complementable right_complementable complementable Element of the carrier of V
{psi} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
Lin {psi} 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
Y + (Lin {psi}) 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 (Y + (Lin {psi})) is non empty set
[: the carrier of (Y + (Lin {psi})),REAL:] is Relation-like non empty set
bool [: the carrier of (Y + (Lin {psi})),REAL:] is non empty set
x is Relation-like the carrier of (Y + (Lin {psi})) -defined REAL -valued Function-like non empty total V18( the carrier of (Y + (Lin {psi})), REAL ) (Y + (Lin {psi})) (Y + (Lin {psi})) (Y + (Lin {psi})) (Y + (Lin {psi})) Element of bool [: the carrier of (Y + (Lin {psi})),REAL:]
x | the carrier of Y is Relation-like the carrier of Y -defined the carrier of (Y + (Lin {psi})) -defined REAL -valued Function-like Element of bool [: the carrier of (Y + (Lin {psi})),REAL:]
rng x is non empty set
dom x is non empty set
the carrier of Y /\ the carrier of X is set
phi is Relation-like Function-like Element of PFuncs ( the carrier of V,REAL)
phi | the carrier of X is Relation-like Function-like set
the carrier of (Lin {psi}) is non empty set
(Lin {psi}) + Y 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 ((Lin {psi}) + Y) is non empty set
dom f9 is non empty set
phi is Relation-like Function-like Element of A
the carrier of RLSY is non empty set
[: the carrier of RLSY,REAL:] is Relation-like non empty set
bool [: the carrier of RLSY,REAL:] is non empty set
ggh is Relation-like the carrier of RLSY -defined REAL -valued Function-like non empty total V18( the carrier of RLSY, REAL ) (RLSY) (RLSY) (RLSY) (RLSY) Element of bool [: the carrier of RLSY,REAL:]
psi is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) (V) (V) Element of bool [: the carrier of V,REAL:]
psi | the carrier of X is Relation-like the carrier of V -defined the carrier of X -defined the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
x is left_complementable right_complementable complementable Element of the carrier of V
psi . x is V31() real ext-real Element of REAL
fi . x is V31() real ext-real Element of REAL
phi is Relation-like the carrier of Y -defined REAL -valued Function-like non empty total V18( the carrier of Y, REAL ) (Y) (Y) (Y) (Y) Element of bool [: the carrier of Y,REAL:]
V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() V160() V161() RealNormSpace-like NORMSTR
the normF of V 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:]
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
||.(fi + q).|| is V31() real ext-real Element of REAL
||.fi.|| is V31() real ext-real Element of REAL
||.q.|| is V31() real ext-real Element of 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
abs q is V31() real ext-real Element of REAL
(abs q) * (X . fi) is V31() real ext-real Element of REAL
||.(q * fi).|| is V31() real ext-real Element of REAL
||.fi.|| is V31() real ext-real Element of REAL
(abs q) * ||.fi.|| 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() V160() V161() RealNormSpace-like NORMSTR
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 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
[: the carrier of X,REAL:] is Relation-like non empty set
bool [: the carrier of X,REAL:] is non empty set
fi is Relation-like the carrier of X -defined REAL -valued Function-like non empty total V18( the carrier of X, REAL ) (X) (X) (X) (X) Element of bool [: the carrier of X,REAL:]
the normF of V 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:]
psi is left_complementable right_complementable complementable Element of the carrier of X
x is left_complementable right_complementable complementable Element of the carrier of V
q is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) Element of bool [: the carrier of V,REAL:]
q . x is V31() real ext-real Element of REAL
||.x.|| is V31() real ext-real Element of REAL
fi . psi is V31() real ext-real Element of REAL
psi is Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) (V) (V) (V) (V) Element of bool [: the carrier of V,REAL:]
psi | the carrier of X is Relation-like the carrier of V -defined the carrier of X -defined the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
x is left_complementable right_complementable complementable Element of the carrier of V
psi . x is V31() real ext-real Element of REAL
||.x.|| is V31() real ext-real Element of REAL
q . x is V31() real ext-real Element of REAL