for V being VectSp of F_Complex
for p being Semi-Norm of V holds p is Banach-Functional of (RealVS V)