:: LOPBAN_2 semantic presentation

REAL is non empty V46() V51() V52() V53() V57() set

NAT is V51() V52() V53() V54() V55() V56() V57() Element of bool REAL

bool REAL is set

COMPLEX is non empty V46() V51() V57() set

RAT is non empty V46() V51() V52() V53() V54() V57() set

INT is non empty V46() V51() V52() V53() V54() V55() V57() set

[:COMPLEX,COMPLEX:] is V15() V36() set

bool [:COMPLEX,COMPLEX:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is V15() V36() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:REAL,REAL:] is V15() V36() V37() V38() set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is V15() V36() V37() V38() set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is V15() V19( RAT ) V36() V37() V38() set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is V15() V19( RAT ) V36() V37() V38() set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() V39() set

[:[:NAT,NAT:],NAT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() V39() set

bool [:[:NAT,NAT:],NAT:] is set

[:NAT,REAL:] is V15() V36() V37() V38() set

bool [:NAT,REAL:] is set

omega is V51() V52() V53() V54() V55() V56() V57() set

bool omega is set

bool NAT is set

the_set_of_RealSequences is non empty set

[:the_set_of_RealSequences,the_set_of_RealSequences:] is V15() set

[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is V15() set

bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is set

[:REAL,the_set_of_RealSequences:] is V15() set

[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is V15() set

bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is set

Linear_Space_of_RealSequences is RLSStruct

the carrier of Linear_Space_of_RealSequences is set

bool the carrier of Linear_Space_of_RealSequences is set

the_set_of_l2RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences

[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is V15() set

[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is V15() V36() V37() V38() set

bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is set

the_set_of_l1RealSequences is non empty Element of bool the carrier of Linear_Space_of_RealSequences

[:the_set_of_l1RealSequences,REAL:] is V15() V36() V37() V38() set

bool [:the_set_of_l1RealSequences,REAL:] is set

[:COMPLEX,REAL:] is V15() V36() V37() V38() set

bool [:COMPLEX,REAL:] is set

{} is empty V15() non-empty empty-yielding V19( RAT ) Function-like one-to-one constant functional V36() V37() V38() V39() V51() V52() V53() V54() V55() V56() V57() set

1 is non empty natural V11() real V13() V32() ext-real positive non negative V51() V52() V53() V54() V55() V56() Element of NAT

0 is empty natural V11() real V13() V15() non-empty empty-yielding V19( RAT ) Function-like one-to-one constant functional V32() ext-real non positive non negative V36() V37() V38() V39() V51() V52() V53() V54() V55() V56() V57() Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

Zeroseq is Element of the_set_of_RealSequences

l1_Space is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of l1_Space is non empty set

0. l1_Space is V80( l1_Space ) left_complementable right_complementable complementable Element of the carrier of l1_Space

the ZeroF of l1_Space is left_complementable right_complementable complementable Element of the carrier of l1_Space

[:NAT, the carrier of l1_Space:] is V15() set

bool [:NAT, the carrier of l1_Space:] 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() RLSStruct

the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

UNIT 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 UNIT is non empty set

[: the carrier of c

bool [: the carrier of c

[: the carrier of X, the carrier of UNIT:] is V15() set

bool [: the carrier of X, the carrier of UNIT:] is set

MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c

ADD is non empty V15() Function-like V25( the carrier of c

ADD * MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]

BS is left_complementable right_complementable complementable Element of the carrier of X

BLOP is V11() real ext-real Element of REAL

BLOP * BS is left_complementable right_complementable complementable Element of the carrier of X

the Mult of X is V15() Function-like V25([:REAL, the carrier of X:]) V29([: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 V15() set

[:[:REAL, the carrier of X:], the carrier of X:] is V15() set

bool [:[:REAL, the carrier of X:], the carrier of X:] is set

the Mult of X . (BLOP,BS) is set

(ADD * MULT) . (BLOP * BS) is left_complementable right_complementable complementable Element of the carrier of UNIT

MULT . (BLOP * BS) is left_complementable right_complementable complementable Element of the carrier of c

ADD . (MULT . (BLOP * BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT

MULT . BS is left_complementable right_complementable complementable Element of the carrier of c

BLOP * (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of c

the Mult of c

[:REAL, the carrier of c

[:[:REAL, the carrier of c

bool [:[:REAL, the carrier of c

the Mult of c

ADD . (BLOP * (MULT . BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT

ADD . (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT

BLOP * (ADD . (MULT . BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT

the Mult of UNIT is V15() Function-like V25([:REAL, the carrier of UNIT:]) V29([:REAL, the carrier of UNIT:], the carrier of UNIT) Element of bool [:[:REAL, the carrier of UNIT:], the carrier of UNIT:]

[:REAL, the carrier of UNIT:] is V15() set

[:[:REAL, the carrier of UNIT:], the carrier of UNIT:] is V15() set

bool [:[:REAL, the carrier of UNIT:], the carrier of UNIT:] is set

the Mult of UNIT . (BLOP,(ADD . (MULT . BS))) is set

(ADD * MULT) . BS is left_complementable right_complementable complementable Element of the carrier of UNIT

BLOP * ((ADD * MULT) . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT

the Mult of UNIT . (BLOP,((ADD * MULT) . BS)) is set

BS is left_complementable right_complementable complementable Element of the carrier of X

BLOP is left_complementable right_complementable complementable Element of the carrier of X

BS + BLOP is left_complementable right_complementable complementable Element of the carrier of X

the addF of X is V15() Function-like V25([: the carrier of X, the carrier of X:]) V29([: 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 V15() set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is V15() set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the addF of X . (BS,BLOP) is left_complementable right_complementable complementable Element of the carrier of X

(ADD * MULT) . (BS + BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT

MULT . (BS + BLOP) is left_complementable right_complementable complementable Element of the carrier of c

ADD . (MULT . (BS + BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT

MULT . BS is left_complementable right_complementable complementable Element of the carrier of c

MULT . BLOP is left_complementable right_complementable complementable Element of the carrier of c

(MULT . BS) + (MULT . BLOP) is left_complementable right_complementable complementable Element of the carrier of c

the addF of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the addF of c

ADD . ((MULT . BS) + (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT

ADD . (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT

ADD . (MULT . BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT

(ADD . (MULT . BS)) + (ADD . (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT

the addF of UNIT is V15() Function-like V25([: the carrier of UNIT, the carrier of UNIT:]) V29([: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT) Element of bool [:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:]

[: the carrier of UNIT, the carrier of UNIT:] is V15() set

[:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:] is V15() set

bool [:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:] is set

the addF of UNIT . ((ADD . (MULT . BS)),(ADD . (MULT . BLOP))) is left_complementable right_complementable complementable Element of the carrier of UNIT

(ADD * MULT) . BS is left_complementable right_complementable complementable Element of the carrier of UNIT

((ADD * MULT) . BS) + (ADD . (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT

the addF of UNIT . (((ADD * MULT) . BS),(ADD . (MULT . BLOP))) is left_complementable right_complementable complementable Element of the carrier of UNIT

(ADD * MULT) . BLOP is left_complementable right_complementable complementable Element of the carrier of UNIT

((ADD * MULT) . BS) + ((ADD * MULT) . BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT

the addF of UNIT . (((ADD * MULT) . BS),((ADD * MULT) . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

c

the carrier of c

[: the carrier of X, the carrier of c

bool [: the carrier of X, the carrier of c

UNIT is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of UNIT is non empty set

[: the carrier of c

bool [: the carrier of c

[: the carrier of X, the carrier of UNIT:] is V15() set

bool [: the carrier of X, the carrier of UNIT:] is set

BoundedLinearOperatorsNorm (c

BoundedLinearOperators (c

R_VectorSpace_of_LinearOperators (c

LinearOperators (c

RealVectSpace ( the carrier of c

K138( the carrier of c

FuncZero ( the carrier of c

0. UNIT is V80(UNIT) left_complementable right_complementable complementable Element of the carrier of UNIT

the ZeroF of UNIT is left_complementable right_complementable complementable Element of the carrier of UNIT

K308( the carrier of UNIT, the carrier of c

FuncAdd ( the carrier of c

[:K138( the carrier of c

[:[:K138( the carrier of c

bool [:[:K138( the carrier of c

FuncExtMult ( the carrier of c

[:REAL,K138( the carrier of c

[:[:REAL,K138( the carrier of c

bool [:[:REAL,K138( the carrier of c

RLSStruct(# K138( the carrier of c

the carrier of (RealVectSpace ( the carrier of c

bool the carrier of (RealVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:REAL,(LinearOperators (c

[:[:REAL,(LinearOperators (c

bool [:[:REAL,(LinearOperators (c

RLSStruct(# (LinearOperators (c

the carrier of (R_VectorSpace_of_LinearOperators (c

bool the carrier of (R_VectorSpace_of_LinearOperators (c

[:(BoundedLinearOperators (c

bool [:(BoundedLinearOperators (c

BoundedLinearOperatorsNorm (X,c

BoundedLinearOperators (X,c

R_VectorSpace_of_LinearOperators (X,c

LinearOperators (X,c

RealVectSpace ( the carrier of X,c

K138( the carrier of X, the carrier of c

FuncZero ( the carrier of X,c

0. c

the ZeroF of c

K308( the carrier of c

FuncAdd ( the carrier of X,c

[:K138( the carrier of X, the carrier of c

[:[:K138( the carrier of X, the carrier of c

bool [:[:K138( the carrier of X, the carrier of c

FuncExtMult ( the carrier of X,c

[:REAL,K138( the carrier of X, the carrier of c

[:[:REAL,K138( the carrier of X, the carrier of c

bool [:[:REAL,K138( the carrier of X, the carrier of c

RLSStruct(# K138( the carrier of X, the carrier of c

the carrier of (RealVectSpace ( the carrier of X,c

bool the carrier of (RealVectSpace ( the carrier of X,c

Zero_ ((LinearOperators (X,c

Add_ ((LinearOperators (X,c

[:(LinearOperators (X,c

[:[:(LinearOperators (X,c

bool [:[:(LinearOperators (X,c

Mult_ ((LinearOperators (X,c

[:REAL,(LinearOperators (X,c

[:[:REAL,(LinearOperators (X,c

bool [:[:REAL,(LinearOperators (X,c

RLSStruct(# (LinearOperators (X,c

the carrier of (R_VectorSpace_of_LinearOperators (X,c

bool the carrier of (R_VectorSpace_of_LinearOperators (X,c

[:(BoundedLinearOperators (X,c

bool [:(BoundedLinearOperators (X,c

BoundedLinearOperatorsNorm (X,UNIT) is non empty V15() Function-like V25( BoundedLinearOperators (X,UNIT)) V29( BoundedLinearOperators (X,UNIT), REAL ) V36() V37() V38() Element of bool [:(BoundedLinearOperators (X,UNIT)),REAL:]

BoundedLinearOperators (X,UNIT) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT))

R_VectorSpace_of_LinearOperators (X,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,UNIT) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,UNIT))

RealVectSpace ( the carrier of X,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of UNIT) is non empty functional M4( the carrier of X, the carrier of UNIT)

FuncZero ( the carrier of X,UNIT) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of K138( the carrier of X, the carrier of UNIT)

K308( the carrier of UNIT, the carrier of X,(0. UNIT)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]

FuncAdd ( the carrier of X,UNIT) is V15() Function-like V25([:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):]) V29([:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT)) Element of bool [:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):]

[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):] is V15() set

[:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is V15() set

bool [:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is set

FuncExtMult ( the carrier of X,UNIT) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of UNIT):]) V29([:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):]

[:REAL,K138( the carrier of X, the carrier of UNIT):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is set

RLSStruct(# K138( the carrier of X, the carrier of UNIT),(FuncZero ( the carrier of X,UNIT)),(FuncAdd ( the carrier of X,UNIT)),(FuncExtMult ( the carrier of X,UNIT)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,UNIT)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,UNIT)) is set

Zero_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like Element of LinearOperators (X,UNIT)

Add_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like V25([:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):]) V29([:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):], LinearOperators (X,UNIT)) Element of bool [:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):]

[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):] is V15() set

[:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is V15() set

bool [:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is set

Mult_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like V25([:REAL,(LinearOperators (X,UNIT)):]) V29([:REAL,(LinearOperators (X,UNIT)):], LinearOperators (X,UNIT)) Element of bool [:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):]

[:REAL,(LinearOperators (X,UNIT)):] is V15() set

[:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is V15() set

bool [:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is set

RLSStruct(# (LinearOperators (X,UNIT)),(Zero_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))),(Add_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))),(Mult_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT)) is non empty set

bool the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT)) is set

[:(BoundedLinearOperators (X,UNIT)),REAL:] is V15() V36() V37() V38() set

bool [:(BoundedLinearOperators (X,UNIT)),REAL:] is set

MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c

(BoundedLinearOperatorsNorm (X,c

ADD is non empty V15() Function-like V25( the carrier of c

ADD * MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]

(BoundedLinearOperatorsNorm (c

((BoundedLinearOperatorsNorm (c

(BoundedLinearOperatorsNorm (X,UNIT)) . (ADD * MULT) is V11() real ext-real Element of REAL

R_NormSpace_of_BoundedLinearOperators (X,c

Zero_ ((BoundedLinearOperators (X,c

Add_ ((BoundedLinearOperators (X,c

[:(BoundedLinearOperators (X,c

[:[:(BoundedLinearOperators (X,c

bool [:[:(BoundedLinearOperators (X,c

Mult_ ((BoundedLinearOperators (X,c

[:REAL,(BoundedLinearOperators (X,c

[:[:REAL,(BoundedLinearOperators (X,c

bool [:[:REAL,(BoundedLinearOperators (X,c

NORMSTR(# (BoundedLinearOperators (X,c

the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c

R_NormSpace_of_BoundedLinearOperators (c

Zero_ ((BoundedLinearOperators (c

Add_ ((BoundedLinearOperators (c

[:(BoundedLinearOperators (c

[:[:(BoundedLinearOperators (c

bool [:[:(BoundedLinearOperators (c

Mult_ ((BoundedLinearOperators (c

[:REAL,(BoundedLinearOperators (c

[:[:REAL,(BoundedLinearOperators (c

bool [:[:REAL,(BoundedLinearOperators (c

NORMSTR(# (BoundedLinearOperators (c

the carrier of (R_NormSpace_of_BoundedLinearOperators (c

BLOP is V15() Function-like left_complementable right_complementable complementable Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (c

||.BLOP.|| is V11() real ext-real Element of REAL

the normF of (R_NormSpace_of_BoundedLinearOperators (c

[: the carrier of (R_NormSpace_of_BoundedLinearOperators (c

bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (c

the normF of (R_NormSpace_of_BoundedLinearOperators (c

RBLOP is left_complementable right_complementable complementable Element of the carrier of X

MULT . RBLOP is left_complementable right_complementable complementable Element of the carrier of c

||.(MULT . RBLOP).|| is V11() real ext-real Element of REAL

the normF of c

[: the carrier of c

bool [: the carrier of c

the normF of c

||.BLOP.|| * ||.(MULT . RBLOP).|| is V11() real ext-real Element of REAL

BS is V15() Function-like left_complementable right_complementable complementable Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c

||.BS.|| is V11() real ext-real Element of REAL

the normF of (R_NormSpace_of_BoundedLinearOperators (X,c

[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c

bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c

the normF of (R_NormSpace_of_BoundedLinearOperators (X,c

||.RBLOP.|| is V11() real ext-real Element of REAL

the normF of X is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, REAL ) V36() V37() V38() Element of bool [: the carrier of X,REAL:]

[: the carrier of X,REAL:] is V15() V36() V37() V38() set

bool [: the carrier of X,REAL:] is set

the normF of X . RBLOP is V11() real ext-real Element of REAL

||.BS.|| * ||.RBLOP.|| is V11() real ext-real Element of REAL

||.BLOP.|| * (||.BS.|| * ||.RBLOP.||) is V11() real ext-real Element of REAL

(ADD * MULT) . RBLOP is left_complementable right_complementable complementable Element of the carrier of UNIT

||.((ADD * MULT) . RBLOP).|| is V11() real ext-real Element of REAL

the normF of UNIT is non empty V15() Function-like V25( the carrier of UNIT) V29( the carrier of UNIT, REAL ) V36() V37() V38() Element of bool [: the carrier of UNIT,REAL:]

[: the carrier of UNIT,REAL:] is V15() V36() V37() V38() set

bool [: the carrier of UNIT,REAL:] is set

the normF of UNIT . ((ADD * MULT) . RBLOP) is V11() real ext-real Element of REAL

ADD . (MULT . RBLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT

||.(ADD . (MULT . RBLOP)).|| is V11() real ext-real Element of REAL

the normF of UNIT . (ADD . (MULT . RBLOP)) is V11() real ext-real Element of REAL

||.BLOP.|| * ||.BS.|| is V11() real ext-real Element of REAL

(||.BLOP.|| * ||.BS.||) * ||.RBLOP.|| is V11() real ext-real Element of REAL

seq1 is left_complementable right_complementable complementable Element of the carrier of X

||.seq1.|| is V11() real ext-real Element of REAL

the normF of X . seq1 is V11() real ext-real Element of REAL

(||.BLOP.|| * ||.BS.||) * ||.seq1.|| is V11() real ext-real Element of REAL

(||.BLOP.|| * ||.BS.||) * 1 is V11() real ext-real Element of REAL

(ADD * MULT) . seq1 is left_complementable right_complementable complementable Element of the carrier of UNIT

||.((ADD * MULT) . seq1).|| is V11() real ext-real Element of REAL

the normF of UNIT . ((ADD * MULT) . seq1) is V11() real ext-real Element of REAL

seq1 is V11() real ext-real Element of REAL

RBLOP is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) V165(X,UNIT) V166(X,UNIT) Lipschitzian Element of bool [: the carrier of X, the carrier of UNIT:]

PreNorms RBLOP is non empty V51() V52() V53() Element of bool REAL

{ ||.(RBLOP . b

g1 is left_complementable right_complementable complementable Element of the carrier of X

RBLOP . g1 is left_complementable right_complementable complementable Element of the carrier of UNIT

||.(RBLOP . g1).|| is V11() real ext-real Element of REAL

the normF of UNIT . (RBLOP . g1) is V11() real ext-real Element of REAL

||.g1.|| is V11() real ext-real Element of REAL

the normF of X . g1 is V11() real ext-real Element of REAL

upper_bound (PreNorms RBLOP) is V11() real ext-real Element of REAL

seq1 is left_complementable right_complementable complementable Element of the carrier of X

(ADD * MULT) . seq1 is left_complementable right_complementable complementable Element of the carrier of UNIT

||.((ADD * MULT) . seq1).|| is V11() real ext-real Element of REAL

the normF of UNIT . ((ADD * MULT) . seq1) is V11() real ext-real Element of REAL

||.seq1.|| is V11() real ext-real Element of REAL

the normF of X . seq1 is V11() real ext-real Element of REAL

(((BoundedLinearOperatorsNorm (c

g1 is V11() real ext-real set

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[: the carrier of X, the carrier of X:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

c

UNIT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

UNIT * c

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))

the carrier of X is non empty set

RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)

FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)

0. X is V80(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

K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set

[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:REAL,K138( the carrier of X, the carrier of X):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,X)) is set

Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)

Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set

[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:REAL,(LinearOperators (X,X)):] is V15() set

[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set

BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))

bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set

Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))) is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]

[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):] is V15() set

[:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set

bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set

c

UNIT is Element of BoundedLinearOperators (X,X)

(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (c

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))

the carrier of X is non empty set

RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)

FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)

0. X is V80(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

K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set

[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:REAL,K138( the carrier of X, the carrier of X):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,X)) is set

Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)

Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set

[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:REAL,(LinearOperators (X,X)):] is V15() set

[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set

BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))

bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set

c

modetrans (c

UNIT is Element of BoundedLinearOperators (X,X)

modetrans (UNIT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

(X,(modetrans (c

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))

the carrier of X is non empty set

RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)

FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)

0. X is V80(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

K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set

[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:REAL,K138( the carrier of X, the carrier of X):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,X)) is set

Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)

Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set

[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:REAL,(LinearOperators (X,X)):] is V15() set

[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set

BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))

bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set

Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))) is V15() Function-like V25([:REAL,(BoundedLinearOperators (X,X)):]) V29([:REAL,(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]

[:REAL,(BoundedLinearOperators (X,X)):] is V15() set

[:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set

bool [:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set

UNIT is V11() real ext-real Element of REAL

c

(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (UNIT,c

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))

R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))

the carrier of X is non empty set

RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)

FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)

0. X is V80(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

K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set

[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:REAL,K138( the carrier of X, the carrier of X):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,X)) is set

Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)

Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set

[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:REAL,(LinearOperators (X,X)):] is V15() set

[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set

bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set

[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):] is V15() set

[:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set

bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set

c

UNIT is Element of BoundedLinearOperators (X,X)

MULT is Element of BoundedLinearOperators (X,X)

c

(X,MULT,UNIT) is Element of BoundedLinearOperators (X,X)

modetrans (MULT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

modetrans (UNIT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

(X,(modetrans (MULT,X,X)),(modetrans (UNIT,X,X))) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

c

UNIT is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]

MULT is Element of BoundedLinearOperators (X,X)

ADD is Element of BoundedLinearOperators (X,X)

c

(X,ADD,MULT) is Element of BoundedLinearOperators (X,X)

modetrans (ADD,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

modetrans (MULT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

(X,(modetrans (ADD,X,X)),(modetrans (MULT,X,X))) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]

UNIT . (MULT,ADD) is Element of BoundedLinearOperators (X,X)

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

id the carrier of X is non empty V15() V18( the carrier of X) V19( the carrier of X) Function-like one-to-one V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

c

UNIT is left_complementable right_complementable complementable Element of the carrier of X

c

the addF of X is V15() Function-like V25([: the carrier of X, the carrier of X:]) V29([: 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:], the carrier of X:] is V15() set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the addF of X . (c

(id the carrier of X) . (c

(id the carrier of X) . c

((id the carrier of X) . c

the addF of X . (((id the carrier of X) . c

(id the carrier of X) . UNIT is left_complementable right_complementable complementable Element of the carrier of X

((id the carrier of X) . c

the addF of X . (((id the carrier of X) . c

c

UNIT is V11() real ext-real Element of REAL

UNIT * c

the Mult of X is V15() Function-like V25([:REAL, the carrier of X:]) V29([: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 V15() set

[:[:REAL, the carrier of X:], the carrier of X:] is V15() set

bool [:[:REAL, the carrier of X:], the carrier of X:] is set

the Mult of X . (UNIT,c

(id the carrier of X) . (UNIT * c

(id the carrier of X) . c

UNIT * ((id the carrier of X) . c

the Mult of X . (UNIT,((id the carrier of X) . c

c

(id the carrier of X) . c

||.((id the carrier of X) . c

the normF of X is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, REAL ) V36() V37() V38() Element of bool [: the carrier of X,REAL:]

[: the carrier of X,REAL:] is V15() V36() V37() V38() set

bool [: the carrier of X,REAL:] is set

the normF of X . ((id the carrier of X) . c

||.c

the normF of X . c

1 * ||.c

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

id the carrier of X is non empty V15() V18( the carrier of X) V19( the carrier of X) Function-like one-to-one V25( the carrier of X) V29( 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:] is V15() set

bool [: the carrier of X, the carrier of X:] is set

R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))

RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)

FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)

0. X is V80(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

K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set

[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]

[:REAL,K138( the carrier of X, the carrier of X):] is V15() set

[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set

bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set

RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct

the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set

bool the carrier of (RealVectSpace ( the carrier of X,X)) is set

Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)

Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set

[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]

[:REAL,(LinearOperators (X,X)):] is V15() set

[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set

bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set

RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set

BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))

bool the carrier of