:: CLOPBAN2 semantic presentation

REAL is non empty V46() V57() V58() V59() V63() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() Element of bool REAL

bool REAL is set

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

bool [:NAT,REAL:] is set

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

omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() set

bool omega is set

bool NAT is set

RAT is non empty V46() V57() V58() V59() V60() V63() set

INT is non empty V46() V57() V58() V59() V60() V61() V63() set

[:NAT,COMPLEX:] is V35() set

bool [:NAT,COMPLEX:] is set

the_set_of_ComplexSequences is non empty set

[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:] is set

[:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is set

bool [:[:the_set_of_ComplexSequences,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is set

[:COMPLEX,the_set_of_ComplexSequences:] is set

[:[:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences:] is set

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

Linear_Space_of_ComplexSequences is non empty strict CLSStruct

the carrier of Linear_Space_of_ComplexSequences is non empty set

bool the carrier of Linear_Space_of_ComplexSequences is set

the_set_of_l2ComplexSequences is Element of bool the carrier of Linear_Space_of_ComplexSequences

[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] is set

[:[:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX:] is V35() set

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

the_set_of_l1ComplexSequences is non empty V144( Linear_Space_of_ComplexSequences ) Element of bool the carrier of Linear_Space_of_ComplexSequences

[:the_set_of_l1ComplexSequences,REAL:] is V35() V36() V37() set

bool [:the_set_of_l1ComplexSequences,REAL:] is set

[:COMPLEX,COMPLEX:] is V35() set

bool [:COMPLEX,COMPLEX:] is set

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

bool [:COMPLEX,REAL:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is V35() set

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

[:REAL,REAL:] is V35() V36() V37() set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is V35() V36() V37() set

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

[:RAT,RAT:] is V17( RAT ) V35() V36() V37() set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is V17( RAT ) V35() V36() V37() set

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

[:INT,INT:] is V17( RAT ) V17( INT ) V35() V36() V37() set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is V17( RAT ) V17( INT ) V35() V36() V37() set

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

[:NAT,NAT:] is V17( RAT ) V17( INT ) V35() V36() V37() V38() set

[:[:NAT,NAT:],NAT:] is V17( RAT ) V17( INT ) V35() V36() V37() V38() set

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

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Function-like functional ext-real non positive non negative V57() V58() V59() V60() V61() V62() V63() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V30() V31() ext-real positive non negative V57() V58() V59() V60() V61() V62() Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Function-like functional V30() V31() ext-real non positive non negative V57() V58() V59() V60() V61() V62() V63() Element of NAT

1r is complex Element of COMPLEX

- 1r is complex Element of COMPLEX

|.1r.| is complex real ext-real Element of REAL

Complex_l1_Space is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the carrier of Complex_l1_Space is non empty set

0. Complex_l1_Space is zero right_complementable Element of the carrier of Complex_l1_Space

the ZeroF of Complex_l1_Space is right_complementable Element of the carrier of Complex_l1_Space

CZeroseq is Element of the_set_of_ComplexSequences

[:NAT, the carrier of Complex_l1_Space:] is set

bool [:NAT, the carrier of Complex_l1_Space:] is set

0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Function-like functional ext-real non positive non negative V57() V58() V59() V60() V61() V62() V63() Element of COMPLEX

c

the carrier of c

NRM is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of NRM is non empty set

[: the carrier of c

bool [: the carrier of c

UNIT is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of UNIT is non empty set

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

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

[: the carrier of c

bool [: the carrier of c

MULT is non empty V13() V16( the carrier of c

ADD is non empty V13() V16( the carrier of NRM) V17( the carrier of UNIT) Function-like V23( the carrier of NRM) V27( the carrier of NRM, the carrier of UNIT) V171(NRM,UNIT) V172(NRM,UNIT) Element of bool [: the carrier of NRM, the carrier of UNIT:]

ADD * MULT is non empty V13() V16( the carrier of c

BS is right_complementable Element of the carrier of c

BLOP is complex set

BLOP * BS is right_complementable Element of the carrier of c

the Mult of c

[:COMPLEX, the carrier of c

[:[:COMPLEX, the carrier of c

bool [:[:COMPLEX, the carrier of c

K23(BLOP,BS) is set

the Mult of c

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

MULT . (BLOP * BS) is right_complementable Element of the carrier of NRM

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

MULT . BS is right_complementable Element of the carrier of NRM

BLOP * (MULT . BS) is right_complementable Element of the carrier of NRM

the Mult of NRM is V13() V16([:COMPLEX, the carrier of NRM:]) V17( the carrier of NRM) Function-like V23([:COMPLEX, the carrier of NRM:]) V27([:COMPLEX, the carrier of NRM:], the carrier of NRM) Element of bool [:[:COMPLEX, the carrier of NRM:], the carrier of NRM:]

[:COMPLEX, the carrier of NRM:] is set

[:[:COMPLEX, the carrier of NRM:], the carrier of NRM:] is set

bool [:[:COMPLEX, the carrier of NRM:], the carrier of NRM:] is set

K23(BLOP,(MULT . BS)) is set

the Mult of NRM . K23(BLOP,(MULT . BS)) is set

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

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

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

the Mult of UNIT is V13() V16([:COMPLEX, the carrier of UNIT:]) V17( the carrier of UNIT) Function-like V23([:COMPLEX, the carrier of UNIT:]) V27([:COMPLEX, the carrier of UNIT:], the carrier of UNIT) Element of bool [:[:COMPLEX, the carrier of UNIT:], the carrier of UNIT:]

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

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

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

K23(BLOP,(ADD . (MULT . BS))) is set

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

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

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

K23(BLOP,((ADD * MULT) . BS)) is set

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

BS is right_complementable Element of the carrier of c

BLOP is right_complementable Element of the carrier of c

BS + BLOP is right_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

K23(BS,BLOP) is set

the addF of c

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

MULT . (BS + BLOP) is right_complementable Element of the carrier of NRM

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

MULT . BS is right_complementable Element of the carrier of NRM

MULT . BLOP is right_complementable Element of the carrier of NRM

(MULT . BS) + (MULT . BLOP) is right_complementable Element of the carrier of NRM

the addF of NRM is V13() V16([: the carrier of NRM, the carrier of NRM:]) V17( the carrier of NRM) Function-like V23([: the carrier of NRM, the carrier of NRM:]) V27([: the carrier of NRM, the carrier of NRM:], the carrier of NRM) Element of bool [:[: the carrier of NRM, the carrier of NRM:], the carrier of NRM:]

[: the carrier of NRM, the carrier of NRM:] is set

[:[: the carrier of NRM, the carrier of NRM:], the carrier of NRM:] is set

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

the addF of NRM . ((MULT . BS),(MULT . BLOP)) is right_complementable Element of the carrier of NRM

K23((MULT . BS),(MULT . BLOP)) is set

the addF of NRM . K23((MULT . BS),(MULT . BLOP)) is set

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

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

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

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

the addF of UNIT is V13() V16([: the carrier of UNIT, the carrier of UNIT:]) V17( the carrier of UNIT) Function-like V23([: the carrier of UNIT, the carrier of UNIT:]) V27([: 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 set

[:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:] is 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 right_complementable Element of the carrier of UNIT

K23((ADD . (MULT . BS)),(ADD . (MULT . BLOP))) is set

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

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

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

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

K23(((ADD * MULT) . BS),(ADD . (MULT . BLOP))) is set

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

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

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

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

K23(((ADD * MULT) . BS),((ADD * MULT) . BLOP)) is set

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

c

the carrier of c

NRM is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the carrier of NRM is non empty set

[: the carrier of c

bool [: the carrier of c

UNIT is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

the carrier of UNIT is non empty set

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

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

[: the carrier of c

bool [: the carrier of c

BoundedLinearOperatorsNorm (NRM,UNIT) is non empty V13() V16( BoundedLinearOperators (NRM,UNIT)) V17( REAL ) Function-like V23( BoundedLinearOperators (NRM,UNIT)) V27( BoundedLinearOperators (NRM,UNIT), REAL ) V35() V36() V37() Element of bool [:(BoundedLinearOperators (NRM,UNIT)),REAL:]

BoundedLinearOperators (NRM,UNIT) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (NRM,UNIT))

C_VectorSpace_of_LinearOperators (NRM,UNIT) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

LinearOperators (NRM,UNIT) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of NRM,UNIT))

ComplexVectSpace ( the carrier of NRM,UNIT) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of (ComplexVectSpace ( the carrier of NRM,UNIT)) is non empty set

bool the carrier of (ComplexVectSpace ( the carrier of NRM,UNIT)) is set

Zero_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT))) is V13() Function-like Element of LinearOperators (NRM,UNIT)

Add_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT))) is V13() V16([:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):]) V17( LinearOperators (NRM,UNIT)) Function-like V23([:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):]) V27([:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):], LinearOperators (NRM,UNIT)) Element of bool [:[:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):],(LinearOperators (NRM,UNIT)):]

[:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):] is set

[:[:(LinearOperators (NRM,UNIT)),(LinearOperators (NRM,UNIT)):],(LinearOperators (NRM,UNIT)):] is set

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

Mult_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT))) is V13() V16([:COMPLEX,(LinearOperators (NRM,UNIT)):]) V17( LinearOperators (NRM,UNIT)) Function-like V23([:COMPLEX,(LinearOperators (NRM,UNIT)):]) V27([:COMPLEX,(LinearOperators (NRM,UNIT)):], LinearOperators (NRM,UNIT)) Element of bool [:[:COMPLEX,(LinearOperators (NRM,UNIT)):],(LinearOperators (NRM,UNIT)):]

[:COMPLEX,(LinearOperators (NRM,UNIT)):] is set

[:[:COMPLEX,(LinearOperators (NRM,UNIT)):],(LinearOperators (NRM,UNIT)):] is set

bool [:[:COMPLEX,(LinearOperators (NRM,UNIT)):],(LinearOperators (NRM,UNIT)):] is set

CLSStruct(# (LinearOperators (NRM,UNIT)),(Zero_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT)))),(Add_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT)))),(Mult_ ((LinearOperators (NRM,UNIT)),(ComplexVectSpace ( the carrier of NRM,UNIT)))) #) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct

the carrier of (C_VectorSpace_of_LinearOperators (NRM,UNIT)) is non empty set

bool the carrier of (C_VectorSpace_of_LinearOperators (NRM,UNIT)) is set

[:(BoundedLinearOperators (NRM,UNIT)),REAL:] is V35() V36() V37() set

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

BoundedLinearOperatorsNorm (c

BoundedLinearOperators (c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

[:(BoundedLinearOperators (c

bool [:(BoundedLinearOperators (c

BoundedLinearOperatorsNorm (c

BoundedLinearOperators (c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

[:(BoundedLinearOperators (c

bool [:(BoundedLinearOperators (c

MULT is non empty V13() V16( the carrier of c

(BoundedLinearOperatorsNorm (c

ADD is non empty V13() V16( the carrier of NRM) V17( the carrier of UNIT) Function-like V23( the carrier of NRM) V27( the carrier of NRM, the carrier of UNIT) V171(NRM,UNIT) V172(NRM,UNIT) Lipschitzian Element of bool [: the carrier of NRM, the carrier of UNIT:]

ADD * MULT is non empty V13() V16( the carrier of c

(BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD is complex real ext-real set

((BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (c

(BoundedLinearOperatorsNorm (c

C_NormSpace_of_BoundedLinearOperators (c

Zero_ ((BoundedLinearOperators (c

Add_ ((BoundedLinearOperators (c

[:(BoundedLinearOperators (c

[:[:(BoundedLinearOperators (c

bool [:[:(BoundedLinearOperators (c

Mult_ ((BoundedLinearOperators (c

[:COMPLEX,(BoundedLinearOperators (c

[:[:COMPLEX,(BoundedLinearOperators (c

bool [:[:COMPLEX,(BoundedLinearOperators (c

CNORMSTR(# (BoundedLinearOperators (c

the carrier of (C_NormSpace_of_BoundedLinearOperators (c

C_NormSpace_of_BoundedLinearOperators (NRM,UNIT) is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR

Zero_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT))) is Element of BoundedLinearOperators (NRM,UNIT)

Add_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT))) is V13() V16([:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):]) V17( BoundedLinearOperators (NRM,UNIT)) Function-like V23([:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):]) V27([:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):], BoundedLinearOperators (NRM,UNIT)) Element of bool [:[:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):]

[:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):] is set

[:[:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):] is set

bool [:[:(BoundedLinearOperators (NRM,UNIT)),(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):] is set

Mult_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT))) is V13() V16([:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):]) V17( BoundedLinearOperators (NRM,UNIT)) Function-like V23([:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):]) V27([:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):], BoundedLinearOperators (NRM,UNIT)) Element of bool [:[:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):]

[:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):] is set

[:[:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):] is set

bool [:[:COMPLEX,(BoundedLinearOperators (NRM,UNIT)):],(BoundedLinearOperators (NRM,UNIT)):] is set

CNORMSTR(# (BoundedLinearOperators (NRM,UNIT)),(Zero_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT)))),(Add_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT)))),(Mult_ ((BoundedLinearOperators (NRM,UNIT)),(C_VectorSpace_of_LinearOperators (NRM,UNIT)))),(BoundedLinearOperatorsNorm (NRM,UNIT)) #) is non empty strict CNORMSTR

the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)) is non empty set

BLOP is V13() Function-like right_complementable Element of the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT))

||.BLOP.|| is complex real ext-real Element of REAL

the normF of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)) is non empty V13() V16( the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT))) V17( REAL ) Function-like V23( the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT))) V27( the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)), REAL ) V35() V36() V37() Element of bool [: the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)),REAL:]

[: the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)),REAL:] is V35() V36() V37() set

bool [: the carrier of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)),REAL:] is set

the normF of (C_NormSpace_of_BoundedLinearOperators (NRM,UNIT)) . BLOP is complex real ext-real Element of REAL

RBLOP is right_complementable Element of the carrier of c

MULT . RBLOP is right_complementable Element of the carrier of NRM

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

the normF of NRM is non empty V13() V16( the carrier of NRM) V17( REAL ) Function-like V23( the carrier of NRM) V27( the carrier of NRM, REAL ) V35() V36() V37() Element of bool [: the carrier of NRM,REAL:]

[: the carrier of NRM,REAL:] is V35() V36() V37() set

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

the normF of NRM . (MULT . RBLOP) is complex real ext-real Element of REAL

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

BS is V13() Function-like right_complementable Element of the carrier of (C_NormSpace_of_BoundedLinearOperators (c

||.BS.|| is complex real ext-real Element of REAL

the normF of (C_NormSpace_of_BoundedLinearOperators (c

[: the carrier of (C_NormSpace_of_BoundedLinearOperators (c

bool [: the carrier of (C_NormSpace_of_BoundedLinearOperators (c

the normF of (C_NormSpace_of_BoundedLinearOperators (c

||.RBLOP.|| is complex real ext-real Element of REAL

the normF of c

[: the carrier of c

bool [: the carrier of c

the normF of c

||.BS.|| * ||.RBLOP.|| is complex real ext-real Element of REAL

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

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

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

the normF of UNIT is non empty V13() V16( the carrier of UNIT) V17( REAL ) Function-like V23( the carrier of UNIT) V27( the carrier of UNIT, REAL ) V35() V36() V37() Element of bool [: the carrier of UNIT,REAL:]

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

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

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

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

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

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

||.BLOP.|| * ||.BS.|| is complex real ext-real Element of REAL

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

seq1 is right_complementable Element of the carrier of c

||.seq1.|| is complex real ext-real Element of REAL

the normF of c

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

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

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

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

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

seq1 is complex real ext-real Element of REAL

seq is non empty V13() V16( the carrier of c

PreNorms seq is non empty V57() V58() V59() Element of bool REAL

{ ||.(seq . b

g1 is right_complementable Element of the carrier of c

seq . g1 is right_complementable Element of the carrier of UNIT

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

the normF of UNIT . (seq . g1) is complex real ext-real Element of REAL

||.g1.|| is complex real ext-real Element of REAL

the normF of c

upper_bound (PreNorms seq) is complex real ext-real Element of REAL

seq1 is right_complementable Element of the carrier of c

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

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

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

||.seq1.|| is complex real ext-real Element of REAL

the normF of c

(((BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (c

g1 is complex real ext-real set

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

NRM is non empty V13() V16( the carrier of c

UNIT is non empty V13() V16( the carrier of c

UNIT * NRM is V13() Function-like set

c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

BoundedLinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

Add_ ((BoundedLinearOperators (c

[:(BoundedLinearOperators (c

[:[:(BoundedLinearOperators (c

bool [:[:(BoundedLinearOperators (c

NRM is Element of BoundedLinearOperators (c

UNIT is Element of BoundedLinearOperators (c

(Add_ ((BoundedLinearOperators (c

K23(NRM,UNIT) is set

(Add_ ((BoundedLinearOperators (c

c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

BoundedLinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

NRM is Element of BoundedLinearOperators (c

modetrans (NRM,c

[: the carrier of c

bool [: the carrier of c

UNIT is Element of BoundedLinearOperators (c

modetrans (UNIT,c

(c

c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

BoundedLinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

Mult_ ((BoundedLinearOperators (c

[:COMPLEX,(BoundedLinearOperators (c

[:[:COMPLEX,(BoundedLinearOperators (c

bool [:[:COMPLEX,(BoundedLinearOperators (c

UNIT is complex set

NRM is Element of BoundedLinearOperators (c

(Mult_ ((BoundedLinearOperators (c

K23(UNIT,NRM) is set

(Mult_ ((BoundedLinearOperators (c

MULT is complex Element of COMPLEX

(Mult_ ((BoundedLinearOperators (c

K23(MULT,NRM) is set

(Mult_ ((BoundedLinearOperators (c

c

BoundedLinearOperators (c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

[:(BoundedLinearOperators (c

[:[:(BoundedLinearOperators (c

bool [:[:(BoundedLinearOperators (c

NRM is V13() V16([:(BoundedLinearOperators (c

UNIT is Element of BoundedLinearOperators (c

MULT is Element of BoundedLinearOperators (c

NRM . (UNIT,MULT) is Element of BoundedLinearOperators (c

K23(UNIT,MULT) is set

NRM . K23(UNIT,MULT) is set

(c

modetrans (MULT,c

[: the carrier of c

bool [: the carrier of c

modetrans (UNIT,c

(c

NRM is V13() V16([:(BoundedLinearOperators (c

UNIT is V13() V16([:(BoundedLinearOperators (c

MULT is Element of BoundedLinearOperators (c

ADD is Element of BoundedLinearOperators (c

NRM . (MULT,ADD) is Element of BoundedLinearOperators (c

K23(MULT,ADD) is set

NRM . K23(MULT,ADD) is set

(c

modetrans (ADD,c

[: the carrier of c

bool [: the carrier of c

modetrans (MULT,c

(c

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

UNIT . K23(MULT,ADD) is set

c

the carrier of c

id the carrier of c

[: the carrier of c

bool [: the carrier of c

NRM is right_complementable Element of the carrier of c

UNIT is right_complementable Element of the carrier of c

NRM + UNIT is right_complementable Element of the carrier of c

the addF of c

[:[: the carrier of c

bool [:[: the carrier of c

the addF of c

K23(NRM,UNIT) is set

the addF of c

(id the carrier of c

(id the carrier of c

((id the carrier of c

the addF of c

K23(((id the carrier of c

the addF of c

(id the carrier of c

((id the carrier of c

the addF of c

K23(((id the carrier of c

the addF of c

NRM is right_complementable Element of the carrier of c

UNIT is complex set

UNIT * NRM is right_complementable Element of the carrier of c

the Mult of c

[:COMPLEX, the carrier of c

[:[:COMPLEX, the carrier of c

bool [:[:COMPLEX, the carrier of c

K23(UNIT,NRM) is set

the Mult of c

(id the carrier of c

(id the carrier of c

UNIT * ((id the carrier of c

K23(UNIT,((id the carrier of c

the Mult of c

NRM is right_complementable Element of the carrier of c

(id the carrier of c

||.((id the carrier of c

the normF of c

[: the carrier of c

bool [: the carrier of c

the normF of c

||.NRM.|| is complex real ext-real Element of REAL

the normF of c

1 * ||.NRM.|| is complex real ext-real Element of REAL

c

the carrier of c

id the carrier of c

[: the carrier of c

bool [: the carrier of c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

BoundedLinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

MULT is non empty V13() V16( the carrier of c

UNIT is non empty V13() V16( the carrier of c

NRM is non empty V13() V16( the carrier of c

(c

ADD is right_complementable Element of the carrier of c

(c

UNIT . ADD is right_complementable Element of the carrier of c

NRM . (UNIT . ADD) is right_complementable Element of the carrier of c

MULT . ADD is right_complementable Element of the carrier of c

ADD is right_complementable Element of the carrier of c

MULT . ADD is right_complementable Element of the carrier of c

UNIT . ADD is right_complementable Element of the carrier of c

NRM . (UNIT . ADD) is right_complementable Element of the carrier of c

BS is right_complementable Element of the carrier of c

MULT . BS is right_complementable Element of the carrier of c

UNIT . BS is right_complementable Element of the carrier of c

NRM . (UNIT . BS) is right_complementable Element of the carrier of c

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

MULT is non empty V13() V16( the carrier of c

UNIT is non empty V13() V16( the carrier of c

(c

NRM is non empty V13() V16( the carrier of c

(c

(c

(c

ADD is right_complementable Element of the carrier of c

(c

(c

NRM . ((c

MULT . ADD is right_complementable Element of the carrier of c

UNIT . (MULT . ADD) is right_complementable Element of the carrier of c

NRM . (UNIT . (MULT . ADD)) is right_complementable Element of the carrier of c

(c

(c

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

id the carrier of c

UNIT is non empty V13() V16( the carrier of c

UNIT * (id the carrier of c

(id the carrier of c

MULT is right_complementable Element of the carrier of c

((id the carrier of c

NRM is non empty V13() V16( the carrier of c

(c

(c

UNIT . MULT is right_complementable Element of the carrier of c

NRM . (UNIT . MULT) is right_complementable Element of the carrier of c

MULT is right_complementable Element of the carrier of c

(UNIT * (id the carrier of c

(c

(c

NRM . MULT is right_complementable Element of the carrier of c

UNIT . (NRM . MULT) is right_complementable Element of the carrier of c

UNIT . MULT is right_complementable Element of the carrier of c

c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c

bool [:[:(LinearOperators (c

Mult_ ((LinearOperators (c

[:COMPLEX,(LinearOperators (c

[:[:COMPLEX,(LinearOperators (c

bool [:[:COMPLEX,(LinearOperators (c

CLSStruct(# (LinearOperators (c

the carrier of (C_VectorSpace_of_LinearOperators (c

BoundedLinearOperators (c

bool the carrier of (C_VectorSpace_of_LinearOperators (c

MULT is Element of BoundedLinearOperators (c

UNIT is Element of BoundedLinearOperators (c

(c

modetrans (MULT,c

[: the carrier of c

bool [: the carrier of c

modetrans (UNIT,c

(c

NRM is Element of BoundedLinearOperators (c

(c

modetrans ((c

modetrans (NRM,c

(c

(c

(c

(c

modetrans ((c

(c

(c

c

C_VectorSpace_of_LinearOperators (c

LinearOperators (c

the carrier of c

ComplexVectSpace ( the carrier of c

the carrier of (ComplexVectSpace ( the carrier of c

bool the carrier of (ComplexVectSpace ( the carrier of c

Zero_ ((LinearOperators (c

Add_ ((LinearOperators (c

[:(LinearOperators (c

[:[:(LinearOperators (c