begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
theorem Th5:
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
begin
theorem
canceled;
theorem
canceled;
theorem Th13:
begin
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
:: deftheorem HAHNBAN:def 1 :
canceled;
:: deftheorem HAHNBAN:def 2 :
canceled;
:: deftheorem Def3 defines subadditive HAHNBAN:def 3 :
:: deftheorem Def4 defines additive HAHNBAN:def 4 :
:: deftheorem Def5 defines homogeneous HAHNBAN:def 5 :
:: deftheorem Def6 defines positively_homogeneous HAHNBAN:def 6 :
:: deftheorem Def7 defines semi-homogeneous HAHNBAN:def 7 :
:: deftheorem Def8 defines absolutely_homogeneous HAHNBAN:def 8 :
:: deftheorem Def9 defines 0-preserving HAHNBAN:def 9 :
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
begin
Lm1:
for V being RealLinearSpace
for X being Subspace of V
for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
Lm2:
for V being RealLinearSpace holds RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) is RealLinearSpace
Lm3:
for V, V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) holds
for W being Subspace of V st W9 = RLSStruct(# the carrier of W,the ZeroF of W,the addF of W,the Mult of W #) holds
W9 is Subspace of V9
Lm4:
for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) holds
for f being linear-Functional of V9 holds f is linear-Functional of V
Lm5:
for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V9
theorem Th35:
theorem Th36:
theorem