:: LOPBAN_2 semantic presentation

REAL is non empty V46() V51() V52() V53() V57() set
NAT is V51() V52() V53() V54() V55() V56() V57() Element of bool REAL
bool REAL is set
COMPLEX is non empty V46() V51() V57() set
RAT is non empty V46() V51() V52() V53() V54() V57() set
INT is non empty V46() V51() V52() V53() V54() V55() V57() set
[:COMPLEX,COMPLEX:] is V15() V36() set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V15() V36() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is V15() V36() V37() V38() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is V15() V36() V37() V38() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is V15() V19( RAT ) V36() V37() V38() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is V15() V19( RAT ) V36() V37() V38() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() V39() set
[:[:NAT,NAT:],NAT:] is V15() V19( RAT ) V19( INT ) V36() V37() V38() V39() set
bool [:[:NAT,NAT:],NAT:] is set
[:NAT,REAL:] is V15() V36() V37() V38() set
bool [:NAT,REAL:] is set
omega is V51() V52() V53() V54() V55() V56() V57() set
bool omega is set
bool NAT is set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is V15() set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is V15() set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
[:REAL,the_set_of_RealSequences:] is V15() set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is V15() set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is set
Linear_Space_of_RealSequences is RLSStruct
the carrier of Linear_Space_of_RealSequences is set
bool the carrier of Linear_Space_of_RealSequences is set
the_set_of_l2RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is V15() set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is V15() V36() V37() V38() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is set
the_set_of_l1RealSequences is non empty Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l1RealSequences,REAL:] is V15() V36() V37() V38() set
bool [:the_set_of_l1RealSequences,REAL:] is set
[:COMPLEX,REAL:] is V15() V36() V37() V38() set
bool [:COMPLEX,REAL:] is set
{} is empty V15() non-empty empty-yielding V19( RAT ) Function-like one-to-one constant functional V36() V37() V38() V39() V51() V52() V53() V54() V55() V56() V57() set
1 is non empty natural V11() real V13() V32() ext-real positive non negative V51() V52() V53() V54() V55() V56() Element of NAT
0 is empty natural V11() real V13() V15() non-empty empty-yielding V19( RAT ) Function-like one-to-one constant functional V32() ext-real non positive non negative V36() V37() V38() V39() V51() V52() V53() V54() V55() V56() V57() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
Zeroseq is Element of the_set_of_RealSequences
l1_Space is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of l1_Space is non empty set
0. l1_Space is V80( l1_Space ) left_complementable right_complementable complementable Element of the carrier of l1_Space
the ZeroF of l1_Space is left_complementable right_complementable complementable Element of the carrier of l1_Space
[:NAT, the carrier of l1_Space:] is V15() set
bool [:NAT, the carrier of l1_Space:] is set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of X is non empty set
c₂ is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of c₂ is non empty set
[: the carrier of X, the carrier of c₂:] is V15() set
bool [: the carrier of X, the carrier of c₂:] is set
UNIT is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of UNIT is non empty set
[: the carrier of c₂, the carrier of UNIT:] is V15() set
bool [: the carrier of c₂, the carrier of UNIT:] is set
[: the carrier of X, the carrier of UNIT:] is V15() set
bool [: the carrier of X, the carrier of UNIT:] is set
MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c₂) V165(X,c₂) V166(X,c₂) Element of bool [: the carrier of X, the carrier of c₂:]
ADD is non empty V15() Function-like V25( the carrier of c₂) V29( the carrier of c₂, the carrier of UNIT) V165(c₂,UNIT) V166(c₂,UNIT) Element of bool [: the carrier of c₂, the carrier of UNIT:]
ADD * MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]
BS is left_complementable right_complementable complementable Element of the carrier of X
BLOP is V11() real ext-real Element of REAL
BLOP * BS is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V15() Function-like V25([:REAL, the carrier of X:]) V29([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is V15() set
[:[:REAL, the carrier of X:], the carrier of X:] is V15() set
bool [:[:REAL, the carrier of X:], the carrier of X:] is set
the Mult of X . (BLOP,BS) is set
(ADD * MULT) . (BLOP * BS) is left_complementable right_complementable complementable Element of the carrier of UNIT
MULT . (BLOP * BS) is left_complementable right_complementable complementable Element of the carrier of c₂
ADD . (MULT . (BLOP * BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT
MULT . BS is left_complementable right_complementable complementable Element of the carrier of c₂
BLOP * (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of c₂
the Mult of c₂ is V15() Function-like V25([:REAL, the carrier of c₂:]) V29([:REAL, the carrier of c₂:], the carrier of c₂) Element of bool [:[:REAL, the carrier of c₂:], the carrier of c₂:]
[:REAL, the carrier of c₂:] is V15() set
[:[:REAL, the carrier of c₂:], the carrier of c₂:] is V15() set
bool [:[:REAL, the carrier of c₂:], the carrier of c₂:] is set
the Mult of c₂ . (BLOP,(MULT . BS)) is set
ADD . (BLOP * (MULT . BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT
ADD . (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT
BLOP * (ADD . (MULT . BS)) is left_complementable right_complementable complementable Element of the carrier of UNIT
the Mult of UNIT is V15() Function-like V25([:REAL, the carrier of UNIT:]) V29([:REAL, the carrier of UNIT:], the carrier of UNIT) Element of bool [:[:REAL, the carrier of UNIT:], the carrier of UNIT:]
[:REAL, the carrier of UNIT:] is V15() set
[:[:REAL, the carrier of UNIT:], the carrier of UNIT:] is V15() set
bool [:[:REAL, the carrier of UNIT:], the carrier of UNIT:] is set
the Mult of UNIT . (BLOP,(ADD . (MULT . BS))) is set
(ADD * MULT) . BS is left_complementable right_complementable complementable Element of the carrier of UNIT
BLOP * ((ADD * MULT) . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT
the Mult of UNIT . (BLOP,((ADD * MULT) . BS)) is set
BS is left_complementable right_complementable complementable Element of the carrier of X
BLOP is left_complementable right_complementable complementable Element of the carrier of X
BS + BLOP is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V15() Function-like V25([: the carrier of X, the carrier of X:]) V29([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is V15() set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
the addF of X . (BS,BLOP) is left_complementable right_complementable complementable Element of the carrier of X
(ADD * MULT) . (BS + BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT
MULT . (BS + BLOP) is left_complementable right_complementable complementable Element of the carrier of c₂
ADD . (MULT . (BS + BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT
MULT . BS is left_complementable right_complementable complementable Element of the carrier of c₂
MULT . BLOP is left_complementable right_complementable complementable Element of the carrier of c₂
(MULT . BS) + (MULT . BLOP) is left_complementable right_complementable complementable Element of the carrier of c₂
the addF of c₂ is V15() Function-like V25([: the carrier of c₂, the carrier of c₂:]) V29([: 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 V15() set
[:[: the carrier of c₂, the carrier of c₂:], the carrier of c₂:] is V15() set
bool [:[: the carrier of c₂, the carrier of c₂:], the carrier of c₂:] is set
the addF of c₂ . ((MULT . BS),(MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of c₂
ADD . ((MULT . BS) + (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT
ADD . (MULT . BS) is left_complementable right_complementable complementable Element of the carrier of UNIT
ADD . (MULT . BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT
(ADD . (MULT . BS)) + (ADD . (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT
the addF of UNIT is V15() Function-like V25([: the carrier of UNIT, the carrier of UNIT:]) V29([: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT) Element of bool [:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:]
[: the carrier of UNIT, the carrier of UNIT:] is V15() set
[:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:] is V15() set
bool [:[: the carrier of UNIT, the carrier of UNIT:], the carrier of UNIT:] is set
the addF of UNIT . ((ADD . (MULT . BS)),(ADD . (MULT . BLOP))) is left_complementable right_complementable complementable Element of the carrier of UNIT
(ADD * MULT) . BS is left_complementable right_complementable complementable Element of the carrier of UNIT
((ADD * MULT) . BS) + (ADD . (MULT . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT
the addF of UNIT . (((ADD * MULT) . BS),(ADD . (MULT . BLOP))) is left_complementable right_complementable complementable Element of the carrier of UNIT
(ADD * MULT) . BLOP is left_complementable right_complementable complementable Element of the carrier of UNIT
((ADD * MULT) . BS) + ((ADD * MULT) . BLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT
the addF of UNIT . (((ADD * MULT) . BS),((ADD * MULT) . BLOP)) is left_complementable right_complementable complementable Element of the carrier of UNIT
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
c₂ is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of c₂ is non empty set
[: the carrier of X, the carrier of c₂:] is V15() set
bool [: the carrier of X, the carrier of c₂:] is set
UNIT is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of UNIT is non empty set
[: the carrier of c₂, the carrier of UNIT:] is V15() set
bool [: the carrier of c₂, the carrier of UNIT:] is set
[: the carrier of X, the carrier of UNIT:] is V15() set
bool [: the carrier of X, the carrier of UNIT:] is set
BoundedLinearOperatorsNorm (c₂,UNIT) is non empty V15() Function-like V25( BoundedLinearOperators (c₂,UNIT)) V29( BoundedLinearOperators (c₂,UNIT), REAL ) V36() V37() V38() Element of bool [:(BoundedLinearOperators (c₂,UNIT)),REAL:]
BoundedLinearOperators (c₂,UNIT) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (c₂,UNIT))
R_VectorSpace_of_LinearOperators (c₂,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (c₂,UNIT) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of c₂,UNIT))
RealVectSpace ( the carrier of c₂,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of c₂, the carrier of UNIT) is non empty functional M4( the carrier of c₂, the carrier of UNIT)
FuncZero ( the carrier of c₂,UNIT) is V15() Function-like V25( the carrier of c₂) V29( the carrier of c₂, the carrier of UNIT) Element of K138( the carrier of c₂, the carrier of UNIT)
0. UNIT is V80(UNIT) left_complementable right_complementable complementable Element of the carrier of UNIT
the ZeroF of UNIT is left_complementable right_complementable complementable Element of the carrier of UNIT
K308( the carrier of UNIT, the carrier of c₂,(0. UNIT)) is non empty V15() Function-like V25( the carrier of c₂) V29( the carrier of c₂, the carrier of UNIT) Element of bool [: the carrier of c₂, the carrier of UNIT:]
FuncAdd ( the carrier of c₂,UNIT) is V15() Function-like V25([:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):]) V29([:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT)) Element of bool [:[:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):]
[:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):] is V15() set
[:[:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):] is V15() set
bool [:[:K138( the carrier of c₂, the carrier of UNIT),K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):] is set
FuncExtMult ( the carrier of c₂,UNIT) is V15() Function-like V25([:REAL,K138( the carrier of c₂, the carrier of UNIT):]) V29([:REAL,K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT)) Element of bool [:[:REAL,K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):]
[:REAL,K138( the carrier of c₂, the carrier of UNIT):] is V15() set
[:[:REAL,K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):] is V15() set
bool [:[:REAL,K138( the carrier of c₂, the carrier of UNIT):],K138( the carrier of c₂, the carrier of UNIT):] is set
RLSStruct(# K138( the carrier of c₂, the carrier of UNIT),(FuncZero ( the carrier of c₂,UNIT)),(FuncAdd ( the carrier of c₂,UNIT)),(FuncExtMult ( the carrier of c₂,UNIT)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of c₂,UNIT)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of c₂,UNIT)) is set
Zero_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT))) is V15() Function-like Element of LinearOperators (c₂,UNIT)
Add_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT))) is V15() Function-like V25([:(LinearOperators (c₂,UNIT)),(LinearOperators (c₂,UNIT)):]) V29([:(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 V15() set
[:[:(LinearOperators (c₂,UNIT)),(LinearOperators (c₂,UNIT)):],(LinearOperators (c₂,UNIT)):] is V15() set
bool [:[:(LinearOperators (c₂,UNIT)),(LinearOperators (c₂,UNIT)):],(LinearOperators (c₂,UNIT)):] is set
Mult_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT))) is V15() Function-like V25([:REAL,(LinearOperators (c₂,UNIT)):]) V29([:REAL,(LinearOperators (c₂,UNIT)):], LinearOperators (c₂,UNIT)) Element of bool [:[:REAL,(LinearOperators (c₂,UNIT)):],(LinearOperators (c₂,UNIT)):]
[:REAL,(LinearOperators (c₂,UNIT)):] is V15() set
[:[:REAL,(LinearOperators (c₂,UNIT)):],(LinearOperators (c₂,UNIT)):] is V15() set
bool [:[:REAL,(LinearOperators (c₂,UNIT)):],(LinearOperators (c₂,UNIT)):] is set
RLSStruct(# (LinearOperators (c₂,UNIT)),(Zero_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT)))),(Add_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT)))),(Mult_ ((LinearOperators (c₂,UNIT)),(RealVectSpace ( the carrier of c₂,UNIT)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (c₂,UNIT)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (c₂,UNIT)) is set
[:(BoundedLinearOperators (c₂,UNIT)),REAL:] is V15() V36() V37() V38() set
bool [:(BoundedLinearOperators (c₂,UNIT)),REAL:] is set
BoundedLinearOperatorsNorm (X,c₂) is non empty V15() Function-like V25( BoundedLinearOperators (X,c₂)) V29( BoundedLinearOperators (X,c₂), REAL ) V36() V37() V38() Element of bool [:(BoundedLinearOperators (X,c₂)),REAL:]
BoundedLinearOperators (X,c₂) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,c₂))
R_VectorSpace_of_LinearOperators (X,c₂) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,c₂) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,c₂))
RealVectSpace ( the carrier of X,c₂) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of c₂) is non empty functional M4( the carrier of X, the carrier of c₂)
FuncZero ( the carrier of X,c₂) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c₂) Element of K138( the carrier of X, the carrier of c₂)
0. c₂ is V80(c₂) left_complementable right_complementable complementable Element of the carrier of c₂
the ZeroF of c₂ is left_complementable right_complementable complementable Element of the carrier of c₂
K308( the carrier of c₂, the carrier of X,(0. c₂)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c₂) Element of bool [: the carrier of X, the carrier of c₂:]
FuncAdd ( the carrier of X,c₂) is V15() Function-like V25([:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):]) V29([:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂)) Element of bool [:[:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):]
[:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):] is V15() set
[:[:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):] is V15() set
bool [:[:K138( the carrier of X, the carrier of c₂),K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):] is set
FuncExtMult ( the carrier of X,c₂) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of c₂):]) V29([:REAL,K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):]
[:REAL,K138( the carrier of X, the carrier of c₂):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of c₂):],K138( the carrier of X, the carrier of c₂):] is set
RLSStruct(# K138( the carrier of X, the carrier of c₂),(FuncZero ( the carrier of X,c₂)),(FuncAdd ( the carrier of X,c₂)),(FuncExtMult ( the carrier of X,c₂)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,c₂)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,c₂)) is set
Zero_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂))) is V15() Function-like Element of LinearOperators (X,c₂)
Add_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂))) is V15() Function-like V25([:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):]) V29([:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):], LinearOperators (X,c₂)) Element of bool [:[:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):]
[:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):] is V15() set
[:[:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):] is V15() set
bool [:[:(LinearOperators (X,c₂)),(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):] is set
Mult_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂))) is V15() Function-like V25([:REAL,(LinearOperators (X,c₂)):]) V29([:REAL,(LinearOperators (X,c₂)):], LinearOperators (X,c₂)) Element of bool [:[:REAL,(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):]
[:REAL,(LinearOperators (X,c₂)):] is V15() set
[:[:REAL,(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):] is V15() set
bool [:[:REAL,(LinearOperators (X,c₂)):],(LinearOperators (X,c₂)):] is set
RLSStruct(# (LinearOperators (X,c₂)),(Zero_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂)))),(Add_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂)))),(Mult_ ((LinearOperators (X,c₂)),(RealVectSpace ( the carrier of X,c₂)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,c₂)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,c₂)) is set
[:(BoundedLinearOperators (X,c₂)),REAL:] is V15() V36() V37() V38() set
bool [:(BoundedLinearOperators (X,c₂)),REAL:] is set
BoundedLinearOperatorsNorm (X,UNIT) is non empty V15() Function-like V25( BoundedLinearOperators (X,UNIT)) V29( BoundedLinearOperators (X,UNIT), REAL ) V36() V37() V38() Element of bool [:(BoundedLinearOperators (X,UNIT)),REAL:]
BoundedLinearOperators (X,UNIT) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT))
R_VectorSpace_of_LinearOperators (X,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,UNIT) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,UNIT))
RealVectSpace ( the carrier of X,UNIT) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of UNIT) is non empty functional M4( the carrier of X, the carrier of UNIT)
FuncZero ( the carrier of X,UNIT) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of K138( the carrier of X, the carrier of UNIT)
K308( the carrier of UNIT, the carrier of X,(0. UNIT)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]
FuncAdd ( the carrier of X,UNIT) is V15() Function-like V25([:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):]) V29([:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT)) Element of bool [:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):]
[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):] is V15() set
[:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is V15() set
bool [:[:K138( the carrier of X, the carrier of UNIT),K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is set
FuncExtMult ( the carrier of X,UNIT) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of UNIT):]) V29([:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):]
[:REAL,K138( the carrier of X, the carrier of UNIT):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of UNIT):],K138( the carrier of X, the carrier of UNIT):] is set
RLSStruct(# K138( the carrier of X, the carrier of UNIT),(FuncZero ( the carrier of X,UNIT)),(FuncAdd ( the carrier of X,UNIT)),(FuncExtMult ( the carrier of X,UNIT)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,UNIT)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,UNIT)) is set
Zero_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like Element of LinearOperators (X,UNIT)
Add_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like V25([:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):]) V29([:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):], LinearOperators (X,UNIT)) Element of bool [:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):]
[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):] is V15() set
[:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is V15() set
bool [:[:(LinearOperators (X,UNIT)),(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is set
Mult_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT))) is V15() Function-like V25([:REAL,(LinearOperators (X,UNIT)):]) V29([:REAL,(LinearOperators (X,UNIT)):], LinearOperators (X,UNIT)) Element of bool [:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):]
[:REAL,(LinearOperators (X,UNIT)):] is V15() set
[:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is V15() set
bool [:[:REAL,(LinearOperators (X,UNIT)):],(LinearOperators (X,UNIT)):] is set
RLSStruct(# (LinearOperators (X,UNIT)),(Zero_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))),(Add_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))),(Mult_ ((LinearOperators (X,UNIT)),(RealVectSpace ( the carrier of X,UNIT)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,UNIT)) is set
[:(BoundedLinearOperators (X,UNIT)),REAL:] is V15() V36() V37() V38() set
bool [:(BoundedLinearOperators (X,UNIT)),REAL:] is set
MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of c₂) V165(X,c₂) V166(X,c₂) Lipschitzian Element of bool [: the carrier of X, the carrier of c₂:]
(BoundedLinearOperatorsNorm (X,c₂)) . MULT is V11() real ext-real Element of REAL
ADD is non empty V15() Function-like V25( the carrier of c₂) V29( the carrier of c₂, the carrier of UNIT) V165(c₂,UNIT) V166(c₂,UNIT) Lipschitzian Element of bool [: the carrier of c₂, the carrier of UNIT:]
ADD * MULT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) Element of bool [: the carrier of X, the carrier of UNIT:]
(BoundedLinearOperatorsNorm (c₂,UNIT)) . ADD is V11() real ext-real Element of REAL
((BoundedLinearOperatorsNorm (c₂,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (X,c₂)) . MULT) is V11() real ext-real Element of REAL
(BoundedLinearOperatorsNorm (X,UNIT)) . (ADD * MULT) is V11() real ext-real Element of REAL
R_NormSpace_of_BoundedLinearOperators (X,c₂) is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
Zero_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂))) is Element of BoundedLinearOperators (X,c₂)
Add_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂))) is V15() Function-like V25([:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):]) V29([:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):], BoundedLinearOperators (X,c₂)) Element of bool [:[:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):]
[:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):] is V15() set
[:[:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):] is V15() set
bool [:[:(BoundedLinearOperators (X,c₂)),(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):] is set
Mult_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂))) is V15() Function-like V25([:REAL,(BoundedLinearOperators (X,c₂)):]) V29([:REAL,(BoundedLinearOperators (X,c₂)):], BoundedLinearOperators (X,c₂)) Element of bool [:[:REAL,(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):]
[:REAL,(BoundedLinearOperators (X,c₂)):] is V15() set
[:[:REAL,(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):] is V15() set
bool [:[:REAL,(BoundedLinearOperators (X,c₂)):],(BoundedLinearOperators (X,c₂)):] is set
NORMSTR(# (BoundedLinearOperators (X,c₂)),(Zero_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂)))),(Add_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂)))),(Mult_ ((BoundedLinearOperators (X,c₂)),(R_VectorSpace_of_LinearOperators (X,c₂)))),(BoundedLinearOperatorsNorm (X,c₂)) #) is non empty strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂)) is non empty set
R_NormSpace_of_BoundedLinearOperators (c₂,UNIT) is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
Zero_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT))) is Element of BoundedLinearOperators (c₂,UNIT)
Add_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT))) is V15() Function-like V25([:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):]) V29([:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):], BoundedLinearOperators (c₂,UNIT)) Element of bool [:[:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):]
[:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):] is V15() set
[:[:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):] is V15() set
bool [:[:(BoundedLinearOperators (c₂,UNIT)),(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):] is set
Mult_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT))) is V15() Function-like V25([:REAL,(BoundedLinearOperators (c₂,UNIT)):]) V29([:REAL,(BoundedLinearOperators (c₂,UNIT)):], BoundedLinearOperators (c₂,UNIT)) Element of bool [:[:REAL,(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):]
[:REAL,(BoundedLinearOperators (c₂,UNIT)):] is V15() set
[:[:REAL,(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):] is V15() set
bool [:[:REAL,(BoundedLinearOperators (c₂,UNIT)):],(BoundedLinearOperators (c₂,UNIT)):] is set
NORMSTR(# (BoundedLinearOperators (c₂,UNIT)),(Zero_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT)))),(Add_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT)))),(Mult_ ((BoundedLinearOperators (c₂,UNIT)),(R_VectorSpace_of_LinearOperators (c₂,UNIT)))),(BoundedLinearOperatorsNorm (c₂,UNIT)) #) is non empty strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)) is non empty set
BLOP is V15() Function-like left_complementable right_complementable complementable Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT))
||.BLOP.|| is V11() real ext-real Element of REAL
the normF of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)) is non empty V15() Function-like V25( the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT))) V29( the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)), REAL ) V36() V37() V38() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)),REAL:] is V15() V36() V37() V38() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)),REAL:] is set
the normF of (R_NormSpace_of_BoundedLinearOperators (c₂,UNIT)) . BLOP is V11() real ext-real Element of REAL
RBLOP is left_complementable right_complementable complementable Element of the carrier of X
MULT . RBLOP is left_complementable right_complementable complementable Element of the carrier of c₂
||.(MULT . RBLOP).|| is V11() real ext-real Element of REAL
the normF of c₂ is non empty V15() Function-like V25( the carrier of c₂) V29( the carrier of c₂, REAL ) V36() V37() V38() Element of bool [: the carrier of c₂,REAL:]
[: the carrier of c₂,REAL:] is V15() V36() V37() V38() set
bool [: the carrier of c₂,REAL:] is set
the normF of c₂ . (MULT . RBLOP) is V11() real ext-real Element of REAL
||.BLOP.|| * ||.(MULT . RBLOP).|| is V11() real ext-real Element of REAL
BS is V15() Function-like left_complementable right_complementable complementable Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂))
||.BS.|| is V11() real ext-real Element of REAL
the normF of (R_NormSpace_of_BoundedLinearOperators (X,c₂)) is non empty V15() Function-like V25( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂))) V29( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂)), REAL ) V36() V37() V38() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂)),REAL:] is V15() V36() V37() V38() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,c₂)),REAL:] is set
the normF of (R_NormSpace_of_BoundedLinearOperators (X,c₂)) . BS is V11() real ext-real Element of REAL
||.RBLOP.|| is V11() real ext-real Element of REAL
the normF of X is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, REAL ) V36() V37() V38() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is V15() V36() V37() V38() set
bool [: the carrier of X,REAL:] is set
the normF of X . RBLOP is V11() real ext-real Element of REAL
||.BS.|| * ||.RBLOP.|| is V11() real ext-real Element of REAL
||.BLOP.|| * (||.BS.|| * ||.RBLOP.||) is V11() real ext-real Element of REAL
(ADD * MULT) . RBLOP is left_complementable right_complementable complementable Element of the carrier of UNIT
||.((ADD * MULT) . RBLOP).|| is V11() real ext-real Element of REAL
the normF of UNIT is non empty V15() Function-like V25( the carrier of UNIT) V29( the carrier of UNIT, REAL ) V36() V37() V38() Element of bool [: the carrier of UNIT,REAL:]
[: the carrier of UNIT,REAL:] is V15() V36() V37() V38() set
bool [: the carrier of UNIT,REAL:] is set
the normF of UNIT . ((ADD * MULT) . RBLOP) is V11() real ext-real Element of REAL
ADD . (MULT . RBLOP) is left_complementable right_complementable complementable Element of the carrier of UNIT
||.(ADD . (MULT . RBLOP)).|| is V11() real ext-real Element of REAL
the normF of UNIT . (ADD . (MULT . RBLOP)) is V11() real ext-real Element of REAL
||.BLOP.|| * ||.BS.|| is V11() real ext-real Element of REAL
(||.BLOP.|| * ||.BS.||) * ||.RBLOP.|| is V11() real ext-real Element of REAL
seq1 is left_complementable right_complementable complementable Element of the carrier of X
||.seq1.|| is V11() real ext-real Element of REAL
the normF of X . seq1 is V11() real ext-real Element of REAL
(||.BLOP.|| * ||.BS.||) * ||.seq1.|| is V11() real ext-real Element of REAL
(||.BLOP.|| * ||.BS.||) * 1 is V11() real ext-real Element of REAL
(ADD * MULT) . seq1 is left_complementable right_complementable complementable Element of the carrier of UNIT
||.((ADD * MULT) . seq1).|| is V11() real ext-real Element of REAL
the normF of UNIT . ((ADD * MULT) . seq1) is V11() real ext-real Element of REAL
seq1 is V11() real ext-real Element of REAL
RBLOP is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of UNIT) V165(X,UNIT) V166(X,UNIT) Lipschitzian Element of bool [: the carrier of X, the carrier of UNIT:]
PreNorms RBLOP is non empty V51() V52() V53() Element of bool REAL
{ ||.(RBLOP . b₁).|| where b₁ is left_complementable right_complementable complementable Element of the carrier of X : ||.b₁.|| <= 1 } is set
g1 is left_complementable right_complementable complementable Element of the carrier of X
RBLOP . g1 is left_complementable right_complementable complementable Element of the carrier of UNIT
||.(RBLOP . g1).|| is V11() real ext-real Element of REAL
the normF of UNIT . (RBLOP . g1) is V11() real ext-real Element of REAL
||.g1.|| is V11() real ext-real Element of REAL
the normF of X . g1 is V11() real ext-real Element of REAL
upper_bound (PreNorms RBLOP) is V11() real ext-real Element of REAL
seq1 is left_complementable right_complementable complementable Element of the carrier of X
(ADD * MULT) . seq1 is left_complementable right_complementable complementable Element of the carrier of UNIT
||.((ADD * MULT) . seq1).|| is V11() real ext-real Element of REAL
the normF of UNIT . ((ADD * MULT) . seq1) is V11() real ext-real Element of REAL
||.seq1.|| is V11() real ext-real Element of REAL
the normF of X . seq1 is V11() real ext-real Element of REAL
(((BoundedLinearOperatorsNorm (c₂,UNIT)) . ADD) * ((BoundedLinearOperatorsNorm (X,c₂)) . MULT)) * ||.seq1.|| is V11() real ext-real Element of REAL
g1 is V11() real ext-real set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
c₂ is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
UNIT is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
UNIT * c₂ is V15() Function-like set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))
the carrier of X is non empty set
RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)
FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)
0. X is V80(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set
[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:REAL,K138( the carrier of X, the carrier of X):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,X)) is set
Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)
Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set
[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:REAL,(LinearOperators (X,X)):] is V15() set
[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set
BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))
bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set
Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))) is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]
[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):] is V15() set
[:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set
bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set
c₂ is Element of BoundedLinearOperators (X,X)
UNIT is Element of BoundedLinearOperators (X,X)
(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (c₂,UNIT) is Element of BoundedLinearOperators (X,X)
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))
the carrier of X is non empty set
RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)
FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)
0. X is V80(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set
[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:REAL,K138( the carrier of X, the carrier of X):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,X)) is set
Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)
Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set
[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:REAL,(LinearOperators (X,X)):] is V15() set
[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set
BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))
bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set
c₂ is Element of BoundedLinearOperators (X,X)
modetrans (c₂,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
UNIT is Element of BoundedLinearOperators (X,X)
modetrans (UNIT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
(X,(modetrans (c₂,X,X)),(modetrans (UNIT,X,X))) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))
the carrier of X is non empty set
RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)
FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)
0. X is V80(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set
[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:REAL,K138( the carrier of X, the carrier of X):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,X)) is set
Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)
Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set
[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:REAL,(LinearOperators (X,X)):] is V15() set
[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set
BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))
bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set
Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))) is V15() Function-like V25([:REAL,(BoundedLinearOperators (X,X)):]) V29([:REAL,(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]
[:REAL,(BoundedLinearOperators (X,X)):] is V15() set
[:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set
bool [:[:REAL,(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set
UNIT is V11() real ext-real Element of REAL
c₂ is Element of BoundedLinearOperators (X,X)
(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (UNIT,c₂) is Element of BoundedLinearOperators (X,X)
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))
R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))
the carrier of X is non empty set
RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)
FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)
0. X is V80(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set
[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:REAL,K138( the carrier of X, the carrier of X):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,X)) is set
Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)
Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set
[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:REAL,(LinearOperators (X,X)):] is V15() set
[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is set
[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):] is V15() set
[:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is V15() set
bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):] is set
c₂ is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]
UNIT is Element of BoundedLinearOperators (X,X)
MULT is Element of BoundedLinearOperators (X,X)
c₂ . (UNIT,MULT) is Element of BoundedLinearOperators (X,X)
(X,MULT,UNIT) is Element of BoundedLinearOperators (X,X)
modetrans (MULT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
modetrans (UNIT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
(X,(modetrans (MULT,X,X)),(modetrans (UNIT,X,X))) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
c₂ is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]
UNIT is V15() Function-like V25([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):]) V29([:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):], BoundedLinearOperators (X,X)) Element of bool [:[:(BoundedLinearOperators (X,X)),(BoundedLinearOperators (X,X)):],(BoundedLinearOperators (X,X)):]
MULT is Element of BoundedLinearOperators (X,X)
ADD is Element of BoundedLinearOperators (X,X)
c₂ . (MULT,ADD) is Element of BoundedLinearOperators (X,X)
(X,ADD,MULT) is Element of BoundedLinearOperators (X,X)
modetrans (ADD,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
modetrans (MULT,X,X) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
(X,(modetrans (ADD,X,X)),(modetrans (MULT,X,X))) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) V29( the carrier of X, the carrier of X) V165(X,X) V166(X,X) Lipschitzian Element of bool [: the carrier of X, the carrier of X:]
UNIT . (MULT,ADD) is Element of BoundedLinearOperators (X,X)
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
id the carrier of X is non empty V15() V18( the carrier of X) V19( the carrier of X) Function-like one-to-one V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
c₂ is left_complementable right_complementable complementable Element of the carrier of X
UNIT is left_complementable right_complementable complementable Element of the carrier of X
c₂ + UNIT is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V15() Function-like V25([: the carrier of X, the carrier of X:]) V29([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is V15() set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
the addF of X . (c₂,UNIT) is left_complementable right_complementable complementable Element of the carrier of X
(id the carrier of X) . (c₂ + UNIT) is left_complementable right_complementable complementable Element of the carrier of X
(id the carrier of X) . c₂ is left_complementable right_complementable complementable Element of the carrier of X
((id the carrier of X) . c₂) + UNIT is left_complementable right_complementable complementable Element of the carrier of X
the addF of X . (((id the carrier of X) . c₂),UNIT) is left_complementable right_complementable complementable Element of the carrier of X
(id the carrier of X) . UNIT is left_complementable right_complementable complementable Element of the carrier of X
((id the carrier of X) . c₂) + ((id the carrier of X) . UNIT) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X . (((id the carrier of X) . c₂),((id the carrier of X) . UNIT)) is left_complementable right_complementable complementable Element of the carrier of X
c₂ is left_complementable right_complementable complementable Element of the carrier of X
UNIT is V11() real ext-real Element of REAL
UNIT * c₂ is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V15() Function-like V25([:REAL, the carrier of X:]) V29([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is V15() set
[:[:REAL, the carrier of X:], the carrier of X:] is V15() set
bool [:[:REAL, the carrier of X:], the carrier of X:] is set
the Mult of X . (UNIT,c₂) is set
(id the carrier of X) . (UNIT * c₂) is left_complementable right_complementable complementable Element of the carrier of X
(id the carrier of X) . c₂ is left_complementable right_complementable complementable Element of the carrier of X
UNIT * ((id the carrier of X) . c₂) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . (UNIT,((id the carrier of X) . c₂)) is set
c₂ is left_complementable right_complementable complementable Element of the carrier of X
(id the carrier of X) . c₂ is left_complementable right_complementable complementable Element of the carrier of X
||.((id the carrier of X) . c₂).|| is V11() real ext-real Element of REAL
the normF of X is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, REAL ) V36() V37() V38() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is V15() V36() V37() V38() set
bool [: the carrier of X,REAL:] is set
the normF of X . ((id the carrier of X) . c₂) is V11() real ext-real Element of REAL
||.c₂.|| is V11() real ext-real Element of REAL
the normF of X . c₂ is V11() real ext-real Element of REAL
1 * ||.c₂.|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like NORMSTR
the carrier of X is non empty set
id the carrier of X is non empty V15() V18( the carrier of X) V19( the carrier of X) Function-like one-to-one V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is V15() set
bool [: the carrier of X, the carrier of X:] is set
R_VectorSpace_of_LinearOperators (X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
LinearOperators (X,X) is non empty functional Element of bool the carrier of (RealVectSpace ( the carrier of X,X))
RealVectSpace ( the carrier of X,X) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
K138( the carrier of X, the carrier of X) is non empty functional M4( the carrier of X, the carrier of X)
FuncZero ( the carrier of X,X) is V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of K138( the carrier of X, the carrier of X)
0. X is V80(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
K308( the carrier of X, the carrier of X,(0. X)) is non empty V15() Function-like V25( the carrier of X) V29( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
FuncAdd ( the carrier of X,X) is V15() Function-like V25([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):]) V29([:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):] is V15() set
[:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:K138( the carrier of X, the carrier of X),K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
FuncExtMult ( the carrier of X,X) is V15() Function-like V25([:REAL,K138( the carrier of X, the carrier of X):]) V29([:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X)) Element of bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):]
[:REAL,K138( the carrier of X, the carrier of X):] is V15() set
[:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is V15() set
bool [:[:REAL,K138( the carrier of X, the carrier of X):],K138( the carrier of X, the carrier of X):] is set
RLSStruct(# K138( the carrier of X, the carrier of X),(FuncZero ( the carrier of X,X)),(FuncAdd ( the carrier of X,X)),(FuncExtMult ( the carrier of X,X)) #) is non empty strict RLSStruct
the carrier of (RealVectSpace ( the carrier of X,X)) is non empty set
bool the carrier of (RealVectSpace ( the carrier of X,X)) is set
Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like Element of LinearOperators (X,X)
Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:(LinearOperators (X,X)),(LinearOperators (X,X)):]) V29([:(LinearOperators (X,X)),(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:(LinearOperators (X,X)),(LinearOperators (X,X)):] is V15() set
[:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:(LinearOperators (X,X)),(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X))) is V15() Function-like V25([:REAL,(LinearOperators (X,X)):]) V29([:REAL,(LinearOperators (X,X)):], LinearOperators (X,X)) Element of bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):]
[:REAL,(LinearOperators (X,X)):] is V15() set
[:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is V15() set
bool [:[:REAL,(LinearOperators (X,X)):],(LinearOperators (X,X)):] is set
RLSStruct(# (LinearOperators (X,X)),(Zero_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Add_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))),(Mult_ ((LinearOperators (X,X)),(RealVectSpace ( the carrier of X,X)))) #) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X)) is non empty set
BoundedLinearOperators (X,X) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X))
bool the carrier of