theorem :: HAHNBAN1:28

for V being VectSp of F_Complex
for p being Semi-Norm of V
for M being Subspace of V
for l being linear-Functional of M st ( for e being Vector of M
for v being Vector of V st v = e holds
|.(l . e).| <= p . v ) holds
ex L being linear-Functional of V st
( L | the carrier of M = l & ( for e being Vector of V holds |.(L . e).| <= p . e ) )