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

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,