:: 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₁ is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of c₁ is non empty set
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₁, the carrier of NRM:] is set
bool [: the carrier of c₁, the carrier of NRM:] is set
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₁, the carrier of UNIT:] is set
bool [: the carrier of c₁, the carrier of UNIT:] is set
MULT is non empty V13() V16( the carrier of c₁) V17( the carrier of NRM) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of NRM) V171(c₁,NRM) V172(c₁,NRM) Element of bool [: the carrier of c₁, the carrier of NRM:]
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₁) V17( the carrier of UNIT) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of UNIT) Element of bool [: the carrier of c₁, the carrier of UNIT:]
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₁ is V13() V16([:COMPLEX, the carrier of c₁:]) V17( the carrier of c₁) Function-like V23([:COMPLEX, the carrier of c₁:]) V27([:COMPLEX, the carrier of c₁:], the carrier of c₁) Element of bool [:[:COMPLEX, the carrier of c₁:], the carrier of c₁:]
[:COMPLEX, the carrier of c₁:] is set
[:[:COMPLEX, the carrier of c₁:], the carrier of c₁:] is set
bool [:[:COMPLEX, the carrier of c₁:], the carrier of c₁:] is set
K23(BLOP,BS) is set
the Mult of c₁ . K23(BLOP,BS) is set
(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₁ is V13() V16([: the carrier of c₁, the carrier of c₁:]) V17( the carrier of c₁) Function-like V23([: the carrier of c₁, the carrier of c₁:]) V27([: the carrier of c₁, the carrier of c₁:], the carrier of c₁) Element of bool [:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
[:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:] is set
bool [:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:] is set
the addF of c₁ . (BS,BLOP) is right_complementable Element of the carrier of c₁
K23(BS,BLOP) is set
the addF of c₁ . K23(BS,BLOP) is set
(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₁ 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 c₁ is non empty set
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₁, the carrier of NRM:] is set
bool [: the carrier of c₁, the carrier of NRM:] is set
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₁, the carrier of UNIT:] is set
bool [: the carrier of c₁, the carrier of UNIT:] is set
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₁,NRM) is non empty V13() V16( BoundedLinearOperators (c₁,NRM)) V17( REAL ) Function-like V23( BoundedLinearOperators (c₁,NRM)) V27( BoundedLinearOperators (c₁,NRM), REAL ) V35() V36() V37() Element of bool [:(BoundedLinearOperators (c₁,NRM)),REAL:]
BoundedLinearOperators (c₁,NRM) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,NRM))
C_VectorSpace_of_LinearOperators (c₁,NRM) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,NRM) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,NRM))
ComplexVectSpace ( the carrier of c₁,NRM) 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 c₁,NRM)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,NRM)) is set
Zero_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM))) is V13() Function-like Element of LinearOperators (c₁,NRM)
Add_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM))) is V13() V16([:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):]) V17( LinearOperators (c₁,NRM)) Function-like V23([:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):]) V27([:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):], LinearOperators (c₁,NRM)) Element of bool [:[:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):]
[:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):] is set
[:[:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):] is set
bool [:[:(LinearOperators (c₁,NRM)),(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):] is set
Mult_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM))) is V13() V16([:COMPLEX,(LinearOperators (c₁,NRM)):]) V17( LinearOperators (c₁,NRM)) Function-like V23([:COMPLEX,(LinearOperators (c₁,NRM)):]) V27([:COMPLEX,(LinearOperators (c₁,NRM)):], LinearOperators (c₁,NRM)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):]
[:COMPLEX,(LinearOperators (c₁,NRM)):] is set
[:[:COMPLEX,(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,NRM)):],(LinearOperators (c₁,NRM)):] is set
CLSStruct(# (LinearOperators (c₁,NRM)),(Zero_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM)))),(Add_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM)))),(Mult_ ((LinearOperators (c₁,NRM)),(ComplexVectSpace ( the carrier of c₁,NRM)))) #) 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 (c₁,NRM)) is non empty set
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,NRM)) is set
[:(BoundedLinearOperators (c₁,NRM)),REAL:] is V35() V36() V37() set
bool [:(BoundedLinearOperators (c₁,NRM)),REAL:] is set
BoundedLinearOperatorsNorm (c₁,UNIT) is non empty V13() V16( BoundedLinearOperators (c₁,UNIT)) V17( REAL ) Function-like V23( BoundedLinearOperators (c₁,UNIT)) V27( BoundedLinearOperators (c₁,UNIT), REAL ) V35() V36() V37() Element of bool [:(BoundedLinearOperators (c₁,UNIT)),REAL:]
BoundedLinearOperators (c₁,UNIT) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,UNIT))
C_VectorSpace_of_LinearOperators (c₁,UNIT) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,UNIT) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,UNIT))
ComplexVectSpace ( the carrier of c₁,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 c₁,UNIT)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,UNIT)) is set
Zero_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,UNIT))) is V13() Function-like Element of LinearOperators (c₁,UNIT)
Add_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,UNIT))) is V13() V16([:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):]) V17( LinearOperators (c₁,UNIT)) Function-like V23([:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):]) V27([:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):], LinearOperators (c₁,UNIT)) Element of bool [:[:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):]
[:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):] is set
[:[:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):] is set
bool [:[:(LinearOperators (c₁,UNIT)),(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):] is set
Mult_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,UNIT))) is V13() V16([:COMPLEX,(LinearOperators (c₁,UNIT)):]) V17( LinearOperators (c₁,UNIT)) Function-like V23([:COMPLEX,(LinearOperators (c₁,UNIT)):]) V27([:COMPLEX,(LinearOperators (c₁,UNIT)):], LinearOperators (c₁,UNIT)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):]
[:COMPLEX,(LinearOperators (c₁,UNIT)):] is set
[:[:COMPLEX,(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,UNIT)):],(LinearOperators (c₁,UNIT)):] is set
CLSStruct(# (LinearOperators (c₁,UNIT)),(Zero_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,UNIT)))),(Add_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,UNIT)))),(Mult_ ((LinearOperators (c₁,UNIT)),(ComplexVectSpace ( the carrier of c₁,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 (c₁,UNIT)) is non empty set
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,UNIT)) is set
[:(BoundedLinearOperators (c₁,UNIT)),REAL:] is V35() V36() V37() set
bool [:(BoundedLinearOperators (c₁,UNIT)),REAL:] is set
MULT is non empty V13() V16( the carrier of c₁) V17( the carrier of NRM) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of NRM) V171(c₁,NRM) V172(c₁,NRM) Lipschitzian Element of bool [: the carrier of c₁, the carrier of NRM:]
(BoundedLinearOperatorsNorm (c₁,NRM)) . MULT is complex real ext-real set
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₁) V17( the carrier of UNIT) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of UNIT) Element of bool [: the carrier of c₁, the carrier of UNIT:]
(BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD is complex real ext-real set
((BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (c₁,NRM)) . MULT) is complex real ext-real set
(BoundedLinearOperatorsNorm (c₁,UNIT)) . (ADD * MULT) is complex real ext-real set
C_NormSpace_of_BoundedLinearOperators (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
Zero_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM))) is Element of BoundedLinearOperators (c₁,NRM)
Add_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM))) is V13() V16([:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):]) V17( BoundedLinearOperators (c₁,NRM)) Function-like V23([:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):]) V27([:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):], BoundedLinearOperators (c₁,NRM)) Element of bool [:[:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):]
[:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):] is set
[:[:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):] is set
bool [:[:(BoundedLinearOperators (c₁,NRM)),(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):] is set
Mult_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM))) is V13() V16([:COMPLEX,(BoundedLinearOperators (c₁,NRM)):]) V17( BoundedLinearOperators (c₁,NRM)) Function-like V23([:COMPLEX,(BoundedLinearOperators (c₁,NRM)):]) V27([:COMPLEX,(BoundedLinearOperators (c₁,NRM)):], BoundedLinearOperators (c₁,NRM)) Element of bool [:[:COMPLEX,(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):]
[:COMPLEX,(BoundedLinearOperators (c₁,NRM)):] is set
[:[:COMPLEX,(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):] is set
bool [:[:COMPLEX,(BoundedLinearOperators (c₁,NRM)):],(BoundedLinearOperators (c₁,NRM)):] is set
CNORMSTR(# (BoundedLinearOperators (c₁,NRM)),(Zero_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM)))),(Add_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM)))),(Mult_ ((BoundedLinearOperators (c₁,NRM)),(C_VectorSpace_of_LinearOperators (c₁,NRM)))),(BoundedLinearOperatorsNorm (c₁,NRM)) #) is non empty strict CNORMSTR
the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)) is non empty set
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₁,NRM))
||.BS.|| is complex real ext-real Element of REAL
the normF of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)) is non empty V13() V16( the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM))) V17( REAL ) Function-like V23( the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM))) V27( the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)), REAL ) V35() V36() V37() Element of bool [: the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)),REAL:]
[: the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)),REAL:] is V35() V36() V37() set
bool [: the carrier of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)),REAL:] is set
the normF of (C_NormSpace_of_BoundedLinearOperators (c₁,NRM)) . BS is complex real ext-real Element of REAL
||.RBLOP.|| is complex real ext-real Element of REAL
the normF of c₁ is non empty V13() V16( the carrier of c₁) V17( REAL ) Function-like V23( the carrier of c₁) V27( the carrier of c₁, REAL ) V35() V36() V37() Element of bool [: the carrier of c₁,REAL:]
[: the carrier of c₁,REAL:] is V35() V36() V37() set
bool [: the carrier of c₁,REAL:] is set
the normF of c₁ . RBLOP is complex real ext-real Element of REAL
||.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₁ . seq1 is complex real ext-real Element of REAL
(||.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₁) V17( the carrier of UNIT) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of UNIT) V171(c₁,UNIT) V172(c₁,UNIT) Lipschitzian Element of bool [: the carrier of c₁, the carrier of UNIT:]
PreNorms seq is non empty V57() V58() V59() Element of bool REAL
{ ||.(seq . b₁).|| where b₁ is right_complementable Element of the carrier of c₁ : ||.b₁.|| <= 1 } is set
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₁ . g1 is complex real ext-real Element of REAL
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₁ . seq1 is complex real ext-real Element of REAL
(((BoundedLinearOperatorsNorm (NRM,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (c₁,NRM)) . MULT)) * ||.seq1.|| is complex real ext-real Element of REAL
g1 is complex real ext-real set
c₁ 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 c₁ is non empty set
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
NRM is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT * NRM is V13() Function-like set
c₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
Add_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁))) is V13() V16([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V17( BoundedLinearOperators (c₁,c₁)) Function-like V23([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V27([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):], BoundedLinearOperators (c₁,c₁)) Element of bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):]
[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):] is set
[:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
NRM is Element of BoundedLinearOperators (c₁,c₁)
UNIT is Element of BoundedLinearOperators (c₁,c₁)
(Add_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . (NRM,UNIT) is Element of BoundedLinearOperators (c₁,c₁)
K23(NRM,UNIT) is set
(Add_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . K23(NRM,UNIT) is set
c₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
NRM is Element of BoundedLinearOperators (c₁,c₁)
modetrans (NRM,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
UNIT is Element of BoundedLinearOperators (c₁,c₁)
modetrans (UNIT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (NRM,c₁,c₁)),(modetrans (UNIT,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
c₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
Mult_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁))) is V13() V16([:COMPLEX,(BoundedLinearOperators (c₁,c₁)):]) V17( BoundedLinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(BoundedLinearOperators (c₁,c₁)):]) V27([:COMPLEX,(BoundedLinearOperators (c₁,c₁)):], BoundedLinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):]
[:COMPLEX,(BoundedLinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
UNIT is complex set
NRM is Element of BoundedLinearOperators (c₁,c₁)
(Mult_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . (UNIT,NRM) is set
K23(UNIT,NRM) is set
(Mult_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . K23(UNIT,NRM) is set
MULT is complex Element of COMPLEX
(Mult_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . (MULT,NRM) is Element of BoundedLinearOperators (c₁,c₁)
K23(MULT,NRM) is set
(Mult_ ((BoundedLinearOperators (c₁,c₁)),(C_VectorSpace_of_LinearOperators (c₁,c₁)))) . K23(MULT,NRM) is set
c₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):] is set
[:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):] is set
NRM is V13() V16([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V17( BoundedLinearOperators (c₁,c₁)) Function-like V23([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V27([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):], BoundedLinearOperators (c₁,c₁)) Element of bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):]
UNIT is Element of BoundedLinearOperators (c₁,c₁)
MULT is Element of BoundedLinearOperators (c₁,c₁)
NRM . (UNIT,MULT) is Element of BoundedLinearOperators (c₁,c₁)
K23(UNIT,MULT) is set
NRM . K23(UNIT,MULT) is set
(c₁,MULT,UNIT) is Element of BoundedLinearOperators (c₁,c₁)
modetrans (MULT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
modetrans (UNIT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (MULT,c₁,c₁)),(modetrans (UNIT,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
NRM is V13() V16([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V17( BoundedLinearOperators (c₁,c₁)) Function-like V23([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V27([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):], BoundedLinearOperators (c₁,c₁)) Element of bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):]
UNIT is V13() V16([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V17( BoundedLinearOperators (c₁,c₁)) Function-like V23([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):]) V27([:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):], BoundedLinearOperators (c₁,c₁)) Element of bool [:[:(BoundedLinearOperators (c₁,c₁)),(BoundedLinearOperators (c₁,c₁)):],(BoundedLinearOperators (c₁,c₁)):]
MULT is Element of BoundedLinearOperators (c₁,c₁)
ADD is Element of BoundedLinearOperators (c₁,c₁)
NRM . (MULT,ADD) is Element of BoundedLinearOperators (c₁,c₁)
K23(MULT,ADD) is set
NRM . K23(MULT,ADD) is set
(c₁,ADD,MULT) is Element of BoundedLinearOperators (c₁,c₁)
modetrans (ADD,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
modetrans (MULT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (ADD,c₁,c₁)),(modetrans (MULT,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT . (MULT,ADD) is Element of BoundedLinearOperators (c₁,c₁)
UNIT . K23(MULT,ADD) is set
c₁ 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 c₁ is non empty set
id the carrier of c₁ is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like one-to-one V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
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₁ is V13() V16([: the carrier of c₁, the carrier of c₁:]) V17( the carrier of c₁) Function-like V23([: the carrier of c₁, the carrier of c₁:]) V27([: the carrier of c₁, the carrier of c₁:], the carrier of c₁) Element of bool [:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:]
[:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:] is set
bool [:[: the carrier of c₁, the carrier of c₁:], the carrier of c₁:] is set
the addF of c₁ . (NRM,UNIT) is right_complementable Element of the carrier of c₁
K23(NRM,UNIT) is set
the addF of c₁ . K23(NRM,UNIT) is set
(id the carrier of c₁) . (NRM + UNIT) is right_complementable Element of the carrier of c₁
(id the carrier of c₁) . NRM is right_complementable Element of the carrier of c₁
((id the carrier of c₁) . NRM) + UNIT is right_complementable Element of the carrier of c₁
the addF of c₁ . (((id the carrier of c₁) . NRM),UNIT) is right_complementable Element of the carrier of c₁
K23(((id the carrier of c₁) . NRM),UNIT) is set
the addF of c₁ . K23(((id the carrier of c₁) . NRM),UNIT) is set
(id the carrier of c₁) . UNIT is right_complementable Element of the carrier of c₁
((id the carrier of c₁) . NRM) + ((id the carrier of c₁) . UNIT) is right_complementable Element of the carrier of c₁
the addF of c₁ . (((id the carrier of c₁) . NRM),((id the carrier of c₁) . UNIT)) is right_complementable Element of the carrier of c₁
K23(((id the carrier of c₁) . NRM),((id the carrier of c₁) . UNIT)) is set
the addF of c₁ . K23(((id the carrier of c₁) . NRM),((id the carrier of c₁) . UNIT)) is set
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₁ is V13() V16([:COMPLEX, the carrier of c₁:]) V17( the carrier of c₁) Function-like V23([:COMPLEX, the carrier of c₁:]) V27([:COMPLEX, the carrier of c₁:], the carrier of c₁) Element of bool [:[:COMPLEX, the carrier of c₁:], the carrier of c₁:]
[:COMPLEX, the carrier of c₁:] is set
[:[:COMPLEX, the carrier of c₁:], the carrier of c₁:] is set
bool [:[:COMPLEX, the carrier of c₁:], the carrier of c₁:] is set
K23(UNIT,NRM) is set
the Mult of c₁ . K23(UNIT,NRM) is set
(id the carrier of c₁) . (UNIT * NRM) is right_complementable Element of the carrier of c₁
(id the carrier of c₁) . NRM is right_complementable Element of the carrier of c₁
UNIT * ((id the carrier of c₁) . NRM) is right_complementable Element of the carrier of c₁
K23(UNIT,((id the carrier of c₁) . NRM)) is set
the Mult of c₁ . K23(UNIT,((id the carrier of c₁) . NRM)) is set
NRM is right_complementable Element of the carrier of c₁
(id the carrier of c₁) . NRM is right_complementable Element of the carrier of c₁
||.((id the carrier of c₁) . NRM).|| is complex real ext-real Element of REAL
the normF of c₁ is non empty V13() V16( the carrier of c₁) V17( REAL ) Function-like V23( the carrier of c₁) V27( the carrier of c₁, REAL ) V35() V36() V37() Element of bool [: the carrier of c₁,REAL:]
[: the carrier of c₁,REAL:] is V35() V36() V37() set
bool [: the carrier of c₁,REAL:] is set
the normF of c₁ . ((id the carrier of c₁) . NRM) is complex real ext-real Element of REAL
||.NRM.|| is complex real ext-real Element of REAL
the normF of c₁ . NRM is complex real ext-real Element of REAL
1 * ||.NRM.|| is complex real ext-real Element of REAL
c₁ 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 c₁ is non empty set
id the carrier of c₁ is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like one-to-one V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
c₁ 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 c₁ is non empty set
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
MULT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
NRM is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,UNIT,NRM) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
ADD is right_complementable Element of the carrier of c₁
(c₁,UNIT,NRM) . 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₁
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₁ 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 c₁ is non empty set
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
MULT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,MULT,UNIT) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
NRM is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(c₁,MULT,UNIT),NRM) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,UNIT,NRM) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,MULT,(c₁,UNIT,NRM)) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
ADD is right_complementable Element of the carrier of c₁
(c₁,(c₁,MULT,UNIT),NRM) . ADD is right_complementable Element of the carrier of c₁
(c₁,MULT,UNIT) . ADD is right_complementable Element of the carrier of c₁
NRM . ((c₁,MULT,UNIT) . ADD) is right_complementable Element of the carrier of 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₁,UNIT,NRM) . (MULT . ADD) is right_complementable Element of the carrier of c₁
(c₁,MULT,(c₁,UNIT,NRM)) . ADD is right_complementable Element of the carrier of c₁
c₁ 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 c₁ is non empty set
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
id the carrier of c₁ is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like one-to-one V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
UNIT * (id the carrier of c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) Element of bool [: the carrier of c₁, the carrier of c₁:]
(id the carrier of c₁) * UNIT is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) Element of bool [: the carrier of c₁, the carrier of c₁:]
MULT is right_complementable Element of the carrier of c₁
((id the carrier of c₁) * UNIT) . MULT is right_complementable Element of the carrier of c₁
NRM is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,UNIT,NRM) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,UNIT,NRM) . MULT is right_complementable Element of the carrier of 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₁)) . MULT is right_complementable Element of the carrier of c₁
(c₁,NRM,UNIT) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,NRM,UNIT) . MULT is right_complementable Element of the carrier of 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₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:COMPLEX,(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:COMPLEX,(LinearOperators (c₁,c₁)):]) V27([:COMPLEX,(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:COMPLEX,(LinearOperators (c₁,c₁)):] is set
[:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
bool [:[:COMPLEX,(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):] is set
CLSStruct(# (LinearOperators (c₁,c₁)),(Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))),(Mult_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁)))) #) 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 (c₁,c₁)) is non empty set
BoundedLinearOperators (c₁,c₁) is non empty Element of bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁))
bool the carrier of (C_VectorSpace_of_LinearOperators (c₁,c₁)) is set
MULT is Element of BoundedLinearOperators (c₁,c₁)
UNIT is Element of BoundedLinearOperators (c₁,c₁)
(c₁,MULT,UNIT) is Element of BoundedLinearOperators (c₁,c₁)
modetrans (MULT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
[: the carrier of c₁, the carrier of c₁:] is set
bool [: the carrier of c₁, the carrier of c₁:] is set
modetrans (UNIT,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (MULT,c₁,c₁)),(modetrans (UNIT,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
NRM is Element of BoundedLinearOperators (c₁,c₁)
(c₁,(c₁,MULT,UNIT),NRM) is Element of BoundedLinearOperators (c₁,c₁)
modetrans ((c₁,MULT,UNIT),c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
modetrans (NRM,c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans ((c₁,MULT,UNIT),c₁,c₁)),(modetrans (NRM,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,UNIT,NRM) is Element of BoundedLinearOperators (c₁,c₁)
(c₁,(modetrans (UNIT,c₁,c₁)),(modetrans (NRM,c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,MULT,(c₁,UNIT,NRM)) is Element of BoundedLinearOperators (c₁,c₁)
modetrans ((c₁,UNIT,NRM),c₁,c₁) is non empty V13() V16( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (MULT,c₁,c₁)),(modetrans ((c₁,UNIT,NRM),c₁,c₁))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
(c₁,(modetrans (MULT,c₁,c₁)),(c₁,(modetrans (UNIT,c₁,c₁)),(modetrans (NRM,c₁,c₁)))) is non empty V13() V16( the carrier of c₁) V16( the carrier of c₁) V17( the carrier of c₁) V17( the carrier of c₁) Function-like V23( the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V27( the carrier of c₁, the carrier of c₁) V171(c₁,c₁) V172(c₁,c₁) Lipschitzian Element of bool [: the carrier of c₁, the carrier of c₁:]
c₁ is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
C_VectorSpace_of_LinearOperators (c₁,c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
LinearOperators (c₁,c₁) is non empty functional Element of bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁))
the carrier of c₁ is non empty set
ComplexVectSpace ( the carrier of c₁,c₁) 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 c₁,c₁)) is non empty set
bool the carrier of (ComplexVectSpace ( the carrier of c₁,c₁)) is set
Zero_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() Function-like Element of LinearOperators (c₁,c₁)
Add_ ((LinearOperators (c₁,c₁)),(ComplexVectSpace ( the carrier of c₁,c₁))) is V13() V16([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V17( LinearOperators (c₁,c₁)) Function-like V23([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):]) V27([:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):], LinearOperators (c₁,c₁)) Element of bool [:[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):],(LinearOperators (c₁,c₁)):]
[:(LinearOperators (c₁,c₁)),(LinearOperators (c₁,c₁)):] is set
[:[:(LinearOperators (c₁,c₁)