let V be VectSp of F_Complex ; :: thesis: for p being Semi-Norm of V holds p is Banach-Functional of (RealVS V)
let p be Semi-Norm of V; :: thesis: p is Banach-Functional of (RealVS V)
reconsider p1 = p as Functional of (RealVS V) by Th21;
A1: p1 is positively_homogeneous

proof

let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 4 :: thesis: for b₁ being object holds
( b₁ <= 0 or p1 . (b₁ * x) = b₁ * (p1 . x) )
let r be Real; :: thesis: ( r <= 0 or p1 . (r * x) = r * (p1 . x) )
assume A2: r > 0 ; :: thesis: p1 . (r * x) = r * (p1 . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence p1 . (r * x) = |.r.| * (p1 . x) by Def14
.= r * (p1 . x) by A2, ABSVALUE:def 1 ;
:: thesis: verum

end;

p1 is subadditive

proof

let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def 1 :: thesis: p1 . (x + y) <= (p1 . x) + (p1 . y)
A3: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
x + y = x1 + y1 by A3;
hence p1 . (x + y) <= (p1 . x) + (p1 . y) by Def11; :: thesis: verum

end;

hence p is Banach-Functional of (RealVS V) by A1; :: thesis: verum