:: deftheorem Def2 defines # LOPBAN_5:def 2 :
for X, Y being RealNormSpace
for H being sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X
for b₅ being sequence of Y holds
( b₅ = H # x iff for n being Nat holds b₅ . n = (H . n) . x );