for E, F being RealNormSpace
for E1 being SubRealNormSpace of E
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )