:: HAHNBAN1 semantic presentation

Lemma1: for b₁ being non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being Element of b₁ holds b₂ * (- b₃) = - (b₂ * b₃)

proof end;

theorem Th1: :: HAHNBAN1:1

for b₁ being complex number holds abs |.b₁.| = |.b₁.| ;

theorem Th2: :: HAHNBAN1:2

for b₁, b₂, b₃, b₄ being real number holds (b₁ + (b₂ * )) * (b₃ + (b₄ * )) = ((b₁ * b₃) - (b₂ * b₄)) + (((b₁ * b₄) + (b₃ * b₂)) * ) ;

theorem Th3: :: HAHNBAN1:3

for b₁ being Real holds [*b₁,0*] * = [*0,b₁*]

proof end;

theorem Th4: :: HAHNBAN1:4

for b₁ being Real holds |.[*b₁,0*].| = abs b₁

proof end;

theorem Th5: :: HAHNBAN1:5

for b₁ being Element of COMPLEX holds |.b₁.| + (0 * ) = ((b₁ *' ) / (|.b₁.| + (0 * ))) * b₁

proof end;

definition

let c₁, c₂ be Real;
func [**c₁,c₂**] -> Element of F_Complex equals :: HAHNBAN1:def 1
a₁ + (a₂ * );
coherence

proof end;

end;

:: deftheorem Def1 defines [** HAHNBAN1:def 1 :

definition

func i_FC -> Element of F_Complex equals :: HAHNBAN1:def 2
 ;
coherence

proof end;

end;

:: deftheorem Def2 defines i_FC HAHNBAN1:def 2 :

theorem Th6: :: HAHNBAN1:6

( i_FC = [*0,1*] & i_FC = [**0,1**] ) by COMPLEX1:def 8;

theorem Th7: :: HAHNBAN1:7

|.i_FC .| = 1 by COMPLEX1:135;

theorem Th8: :: HAHNBAN1:8

i_FC * i_FC = - (1. F_Complex )

proof end;

theorem Th9: :: HAHNBAN1:9

(- (1. F_Complex )) * (- (1. F_Complex )) = 1. F_Complex

proof end;

theorem Th10: :: HAHNBAN1:10

for b₁, b₂, b₃, b₄ being Real holds [**b₁,b₂**] + [**b₃,b₄**] = [**(b₁ + b₃),(b₂ + b₄)**]

proof end;

theorem Th11: :: HAHNBAN1:11

for b₁, b₂, b₃, b₄ being Real holds [**b₁,b₂**] * [**b₃,b₄**] = [**((b₁ * b₃) - (b₂ * b₄)),((b₁ * b₄) + (b₃ * b₂))**]

proof end;

theorem Th12: :: HAHNBAN1:12

for b₁ being complex number holds abs |.b₁.| = |.b₁.| ;

theorem Th13: :: HAHNBAN1:13

for b₁ being Real holds |.[**b₁,0**].| = abs b₁ ;

theorem Th14: :: HAHNBAN1:14

for b₁ being Real holds [**b₁,0**] * i_FC = [**0,b₁**] by COMPLFLD:6;

theorem Th15: :: HAHNBAN1:15

for b₁, b₂ being Real holds
( Re [**b₁,b₂**] = b₁ & Im [**b₁,b₂**] = b₂ ) by COMPLEX1:28;

theorem Th16: :: HAHNBAN1:16

for b₁, b₂ being Element of F_Complex holds
( Re (b₁ + b₂) = (Re b₁) + (Re b₂) & Im (b₁ + b₂) = (Im b₁) + (Im b₂) )

proof end;

theorem Th17: :: HAHNBAN1:17

for b₁, b₂ being Element of F_Complex holds
( Re (b₁ * b₂) = ((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂)) & Im (b₁ * b₂) = ((Re b₁) * (Im b₂)) + ((Re b₂) * (Im b₁)) )

proof end;

definition

let c₁ be 1-sorted ;
let c₂ be VectSpStr of c₁;
mode Functional of a₂ is Function of the carrier of a₂,the carrier of a₁;

end;

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be Functional of c₂;
canceled;
canceled;
canceled;
func c₃ + c₄ -> Functional of a₂ means :Def6: :: HAHNBAN1:def 6
for b₁ being Element of a₂ holds a₅ . b₁ = (a₃ . b₁) + (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 HAHNBAN1:def 3 :

:: deftheorem Def4 HAHNBAN1:def 4 :

:: deftheorem Def5 HAHNBAN1:def 5 :

:: deftheorem Def6 defines + HAHNBAN1:def 6 :

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
func - c₃ -> Functional of a₂ means :Def7: :: HAHNBAN1:def 7
for b₁ being Element of a₂ holds a₄ . b₁ = - (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - HAHNBAN1:def 7 :

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be Functional of c₂;
func c₃ - c₄ -> Functional of a₂ equals :: HAHNBAN1:def 8
a₃ + (- a₄);
coherence ;

end;

:: deftheorem Def8 defines - HAHNBAN1:def 8 :

definition

let c₁ be non empty HGrStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Element of c₁;
let c₄ be Functional of c₂;
func c₃ * c₄ -> Functional of a₂ means :Def9: :: HAHNBAN1:def 9
for b₁ being Element of a₂ holds a₅ . b₁ = a₃ * (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines * HAHNBAN1:def 9 :

definition

let c₁ be non empty ZeroStr ;
let c₂ be VectSpStr of c₁;
func 0Functional c₂ -> Functional of a₂ equals :: HAHNBAN1:def 10
([#] a₂) --> (0. a₁);
coherence

proof end;

end;

:: deftheorem Def10 defines 0Functional HAHNBAN1:def 10 :

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
attr a₃ is additive means :Def11: :: HAHNBAN1:def 11
for b₁, b₂ being Vector of a₂ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def11 defines additive HAHNBAN1:def 11 :

definition

let c₁ be non empty HGrStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
attr a₃ is homogeneous means :Def12: :: HAHNBAN1:def 12
for b₁ being Vector of a₂
for b₂ being Scalar of holds a₃ . (b₂ * b₁) = b₂ * (a₃ . b₁);

end;

:: deftheorem Def12 defines homogeneous HAHNBAN1:def 12 :

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
attr a₃ is 0-preserving means :: HAHNBAN1:def 13
a₃ . (0. a₂) = 0. a₁;

end;

:: deftheorem Def13 defines 0-preserving HAHNBAN1:def 13 :

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
cluster homogeneous -> 0-preserving Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster 0Functional a₂ -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster 0Functional a₂ -> additive homogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
cluster 0Functional a₂ -> 0-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster additive homogeneous 0-preserving Relation of the carrier of a₂,the carrier of a₁;
existence

proof end;

end;

theorem Th18: :: HAHNBAN1:18

canceled;

theorem Th19: :: HAHNBAN1:19

canceled;

theorem Th20: :: HAHNBAN1:20

for b₁ being non empty Abelian LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃, b₄ being Functional of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th21: :: HAHNBAN1:21

for b₁ being non empty add-associative LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃, b₄, b₅ being Functional of b₂ holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅)

proof end;

theorem Th22: :: HAHNBAN1:22

for b₁ being non empty ZeroStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Element of b₂ holds (0Functional b₂) . b₃ = 0. b₁

proof end;

theorem Th23: :: HAHNBAN1:23

for b₁ being non empty right_zeroed LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Functional of b₂ holds b₃ + (0Functional b₂) = b₃

proof end;

theorem Th24: :: HAHNBAN1:24

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Functional of b₂ holds b₃ - b₃ = 0Functional b₂

proof end;

theorem Th25: :: HAHNBAN1:25

for b₁ being non empty right-distributive doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Element of b₁
for b₄, b₅ being Functional of b₂ holds b₃ * (b₄ + b₅) = (b₃ * b₄) + (b₃ * b₅)

proof end;

theorem Th26: :: HAHNBAN1:26

for b₁ being non empty left-distributive doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃, b₄ being Element of b₁
for b₅ being Functional of b₂ holds (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅)

proof end;

theorem Th27: :: HAHNBAN1:27

for b₁ being non empty associative HGrStr
for b₂ being non empty VectSpStr of b₁
for b₃, b₄ being Element of b₁
for b₅ being Functional of b₂ holds (b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th28: :: HAHNBAN1:28

for b₁ being non empty left_unital doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Functional of b₂ holds (1. b₁) * b₃ = b₃

proof end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be additive Functional of c₂;
cluster a₃ + a₄ -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be additive Functional of c₂;
cluster - a₃ -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Element of c₁;
let c₄ be additive Functional of c₂;
cluster a₃ * a₄ -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be homogeneous Functional of c₂;
cluster a₃ + a₄ -> homogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be homogeneous Functional of c₂;
cluster - a₃ -> homogeneous ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Element of c₁;
let c₄ be homogeneous Functional of c₂;
cluster a₃ * a₄ -> homogeneous ;
coherence

proof end;

end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
mode linear-Functional of a₂ is additive homogeneous Functional of a₂;

end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
func c₂ *' -> non empty strict VectSpStr of a₁ means :Def14: :: HAHNBAN1:def 14
( ( for b₁ being set holds
( b₁ in the carrier of a₃ iff b₁ is linear-Functional of a₂ ) ) & ( for b₁, b₂ being linear-Functional of a₂ holds the add of a₃ . b₁,b₂ = b₁ + b₂ ) & the Zero of a₃ = 0Functional a₂ & ( for b₁ being linear-Functional of a₂
for b₂ being Element of a₁ holds the lmult of a₃ . b₂,b₁ = b₂ * b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines *' HAHNBAN1:def 14 :

registration

proof end;

end;

registration

proof end;

cluster a₂ *' -> non empty Abelian right_zeroed strict ;
coherence

proof end;

cluster a₂ *' -> non empty Abelian right_complementable strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster a₂ *' -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like ;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be VectSpStr of c₁;
mode RFunctional of a₂ is Function of the carrier of a₂, REAL ;

end;

definition

let c₁ be 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be RFunctional of c₂;
canceled;
attr a₃ is subadditive means :Def16: :: HAHNBAN1:def 16
for b₁, b₂ being Vector of a₂ holds a₃ . (b₁ + b₂) <= (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def15 HAHNBAN1:def 15 :

:: deftheorem Def16 defines subadditive HAHNBAN1:def 16 :

definition

let c₁ be 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be RFunctional of c₂;
attr a₃ is additive means :Def17: :: HAHNBAN1:def 17
for b₁, b₂ being Vector of a₂ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def17 defines additive HAHNBAN1:def 17 :

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be RFunctional of c₁;
attr a₂ is Real_homogeneous means :Def18: :: HAHNBAN1:def 18
for b₁ being Vector of a₁
for b₂ being Real holds a₂ . ([**b₂,0**] * b₁) = b₂ * (a₂ . b₁);

end;

:: deftheorem Def18 defines Real_homogeneous HAHNBAN1:def 18 :

theorem Th29: :: HAHNBAN1:29

for b₁ being non empty VectSp-like VectSpStr of F_Complex
for b₂ being RFunctional of b₁ st b₂ is Real_homogeneous holds
for b₃ being Vector of b₁
for b₄ being Real holds b₂ . ([**0,b₄**] * b₃) = b₄ * (b₂ . (i_FC * b₃))

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be RFunctional of c₁;
attr a₂ is homogeneous means :Def19: :: HAHNBAN1:def 19
for b₁ being Vector of a₁
for b₂ being Scalar of holds a₂ . (b₂ * b₁) = |.b₂.| * (a₂ . b₁);

end;

:: deftheorem Def19 defines homogeneous HAHNBAN1:def 19 :

definition

let c₁ be 1-sorted ;
let c₂ be VectSpStr of c₁;
let c₃ be RFunctional of c₂;
attr a₃ is 0-preserving means :: HAHNBAN1:def 20
a₃ . (0. a₂) = 0;

end;

:: deftheorem Def20 defines 0-preserving HAHNBAN1:def 20 :

registration

let c₁ be 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
cluster additive -> subadditive Relation of the carrier of a₂, REAL ;
coherence

proof end;

end;

Lemma32: 0c = [*0,0*]
by ARYTM_0:def 7, COMPLEX1:def 6;

Lemma33: 1r = [*1,0*]
by ARYTM_0:def 7, COMPLEX1:def 7;

registration

let c₁ be VectSp of F_Complex ;
cluster Real_homogeneous -> 0-preserving Relation of the carrier of a₁, REAL ;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be VectSpStr of c₁;
func 0RFunctional c₂ -> RFunctional of a₂ equals :: HAHNBAN1:def 21
([#] a₂) --> 0;
coherence

proof end;

end;

:: deftheorem Def21 defines 0RFunctional HAHNBAN1:def 21 :

registration

let c₁ be 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
cluster 0RFunctional a₂ -> subadditive additive ;
coherence

proof end;

cluster 0RFunctional a₂ -> 0-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster 0RFunctional a₁ -> subadditive additive Real_homogeneous 0-preserving ;
coherence

proof end;

cluster 0RFunctional a₁ -> subadditive additive homogeneous 0-preserving ;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
cluster subadditive additive 0-preserving Relation of the carrier of a₂, REAL ;
existence

proof end;

end;

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster subadditive additive Real_homogeneous homogeneous Relation of the carrier of a₁, REAL ;
existence

proof end;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
mode Semi-Norm of a₁ is subadditive homogeneous RFunctional of a₁;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
func RealVS c₁ -> strict RLSStruct means :Def22: :: HAHNBAN1:def 22
( LoopStr(# the carrier of a₂,the add of a₂,the Zero of a₂ #) = LoopStr(# the carrier of a₁,the add of a₁,the Zero of a₁ #) & ( for b₁ being Real
for b₂ being Vector of a₁ holds the Mult of a₂ . b₁,b₂ = [**b₁,0**] * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines RealVS HAHNBAN1:def 22 :

registration

let c₁ be non empty VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict Abelian ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict add-associative ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict right_zeroed ;
coherence

proof end;

end;

registration

let c₁ be non empty right_complementable VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict right_complementable ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSp-like VectSpStr of F_Complex ;
cluster RealVS a₁ -> non empty strict RealLinearSpace-like ;
coherence

proof end;

end;

theorem Th30: :: HAHNBAN1:30

for b₁ being non empty VectSp of F_Complex
for b₂ being Subspace of b₁ holds RealVS b₂ is Subspace of RealVS b₁

proof end;

theorem Th31: :: HAHNBAN1:31

for b₁ being non empty VectSpStr of F_Complex
for b₂ being RFunctional of b₁ holds b₂ is Functional of (RealVS b₁)

proof end;

theorem Th32: :: HAHNBAN1:32

for b₁ being non empty VectSp of F_Complex
for b₂ being Semi-Norm of b₁ holds b₂ is Banach-Functional of (RealVS b₁)

proof end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
func projRe c₂ -> Functional of (RealVS a₁) means :Def23: :: HAHNBAN1:def 23
for b₁ being Element of a₁ holds a₃ . b₁ = Re (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines projRe HAHNBAN1:def 23 :

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of c₁;
func projIm c₂ -> Functional of (RealVS a₁) means :Def24: :: HAHNBAN1:def 24
for b₁ being Element of a₁ holds a₃ . b₁ = Im (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines projIm HAHNBAN1:def 24 :

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of (RealVS c₁);
func RtoC c₂ -> RFunctional of a₁ equals :: HAHNBAN1:def 25
a₂;
coherence

proof end;

end;

:: deftheorem Def25 defines RtoC HAHNBAN1:def 25 :

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be RFunctional of c₁;
func CtoR c₂ -> Functional of (RealVS a₁) equals :: HAHNBAN1:def 26
a₂;
coherence

proof end;

end;

:: deftheorem Def26 defines CtoR HAHNBAN1:def 26 :

registration

let c₁ be non empty VectSp of F_Complex ;
let c₂ be additive Functional of (RealVS c₁);
cluster RtoC a₂ -> subadditive additive ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSp of F_Complex ;
let c₂ be additive RFunctional of c₁;
cluster CtoR a₂ -> additive ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSp of F_Complex ;
let c₂ be homogeneous Functional of (RealVS c₁);
cluster RtoC a₂ -> Real_homogeneous 0-preserving ;
coherence

proof end;

end;

registration

let c₁ be non empty VectSp of F_Complex ;
let c₂ be Real_homogeneous RFunctional of c₁;
cluster CtoR a₂ -> homogeneous ;
coherence

proof end;

end;

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be RFunctional of c₁;
func i-shift c₂ -> RFunctional of a₁ means :Def27: :: HAHNBAN1:def 27
for b₁ being Element of a₁ holds a₃ . b₁ = a₂ . (i_FC * b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines i-shift HAHNBAN1:def 27 :

definition

let c₁ be non empty VectSpStr of F_Complex ;
let c₂ be Functional of (RealVS c₁);
func prodReIm c₂ -> Functional of a₁ means :Def28: :: HAHNBAN1:def 28
for b₁ being Element of a₁ holds a₃ . b₁ = [**((RtoC a₂) . b₁),(- ((i-shift (RtoC a₂)) . b₁))**];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines prodReIm HAHNBAN1:def 28 :

theorem Th33: :: HAHNBAN1:33

for b₁ being non empty VectSp of F_Complex
for b₂ being linear-Functional of b₁ holds projRe b₂ is linear-Functional of (RealVS b₁)

proof end;

theorem Th34: :: HAHNBAN1:34

for b₁ being non empty VectSp of F_Complex
for b₂ being linear-Functional of b₁ holds projIm b₂ is linear-Functional of (RealVS b₁)

proof end;

theorem Th35: :: HAHNBAN1:35

for b₁ being non empty VectSp of F_Complex
for b₂ being linear-Functional of (RealVS b₁) holds prodReIm b₂ is linear-Functional of b₁

proof end;

theorem Th36: :: HAHNBAN1:36

for b₁ being non empty VectSp of F_Complex
for b₂ being Semi-Norm of b₁
for b₃ being Subspace of b₁
for b₄ being linear-Functional of b₃ st ( for b₅ being Vector of b₃
for b₆ being Vector of b₁ st b₆ = b₅ holds
|.(b₄ . b₅).| <= b₂ . b₆ ) holds
ex b₅ being linear-Functional of b₁ st
( b₅ | the carrier of b₃ = b₄ & ( for b₆ being Vector of b₁ holds |.(b₅ . b₆).| <= b₂ . b₆ ) )

proof end;