hahnban1.miz

begin



 Lm1: for F be add-associative right_zeroed right_complementable Abelian right-distributive non empty doubleLoopStr holds for x,y be Element of F holds (x * ( - y)) = ( - (x * y))

 proof

 let F be add-associative right_zeroed right_complementable Abelian right-distributive non empty doubleLoopStr;

 let x,y be Element of F;

 ((x * y) + (x * ( - y))) = (x * (y + ( - y))) by VECTSP_1:def 2

 .= (x * ( 0. F)) by RLVECT_1:def 10

 .= ( 0. F);

 hence thesis by RLVECT_1:def 10;

 end;

 ::$Canceled

 theorem :: HAHNBAN1:2

 for x1,y1,x2,y2 be Real holds ((x1 + (y1 * )) * (x2 + (y2 * ))) = (((x1 * x2) - (y1 * y2)) + (((x1 * y2) + (x2 * y1)) * ));

 theorem :: HAHNBAN1:3



 Th2: for z be Element of COMPLEX holds ( |.z.| + ( 0 * )) = (((z *' ) / ( |.z.| + ( 0 * ))) * z)

 proof

 let z be Element of COMPLEX ;

 per cases ;

 suppose

 A1: |.z.| = 0 ;

 then z = 0 by COMPLEX1: 45;

 hence thesis by A1;

 end;

 suppose

 A2: |.z.| <> 0 ;



 A3: ( Im (z * (z *' ))) = 0 by COMPLEX1: 40;

 |.z.| = ( |.z.| + ( 0 * ));

 then

 A4: ( Re |.z.|) = |.z.| & ( Im |.z.|) = 0 by COMPLEX1: 12;



 A5: (((z *' ) / |.z.|) * z) = ((z * (z *' )) / |.z.|) & ( Re (z * (z *' ))) = ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 40, XCMPLX_1: 74;

 then

 A6: ( Im (((z *' ) / |.z.|) * z)) = ((( |.z.| * 0 ) - (((( Re z) ^2 ) + (( Im z) ^2 )) * 0 )) / (( |.z.| ^2 ) + ( 0 ^2 ))) by A3, A4, COMPLEX1: 24;

 ( Re (((z *' ) / |.z.|) * z)) = (((((( Re z) ^2 ) + (( Im z) ^2 )) * |.z.|) + ( 0 * 0 )) / (( |.z.| ^2 ) + ( 0 ^2 ))) by A5, A3, A4, COMPLEX1: 24

 .= (( |.(z * z).| * |.z.|) / ( |.z.| * |.z.|)) by COMPLEX1: 68

 .= ( |.(z * z).| / |.z.|) by A2, XCMPLX_1: 91

 .= (( |.z.| * |.z.|) / |.z.|) by COMPLEX1: 65

 .= |.z.| by A2, XCMPLX_1: 89;

 hence thesis by A6, COMPLEX1: 13;

 end;

 end;

 begin

 definition

 let x,y be Real;

 :: HAHNBAN1:def1

 func [**x,y**] -> Element of F_Complex equals (x + (y * ));

 coherence

 proof

 (x + (y * )) in COMPLEX by XCMPLX_0:def 2;

 hence thesis by COMPLFLD:def 1;

 end;

 end

 definition

 :: HAHNBAN1:def2

 func i_FC -> Element of F_Complex equals ;

 coherence

 proof

 ( 0 + (1 * )) = [** 0 , 1**];

 hence thesis;

 end;

 end

 theorem :: HAHNBAN1:4



 Th3: ( i_FC * i_FC ) = ( - ( 1_ F_Complex ))

 proof



 thus ( i_FC * i_FC ) = ( - 1r )

 .= ( - ( 1_ F_Complex )) by COMPLFLD: 2, COMPLFLD: 8;

 end;

 theorem :: HAHNBAN1:5



 Th4: (( - ( 1_ F_Complex )) * ( - ( 1_ F_Complex ))) = ( 1_ F_Complex )

 proof

 ( - 1r ) = ( - ( 1_ F_Complex )) by COMPLFLD: 2, COMPLFLD: 8;

 hence thesis by COMPLFLD: 8;

 end;

 theorem :: HAHNBAN1:6

 for x1,y1,x2,y2 be Real holds ( [**x1, y1**] + [**x2, y2**]) = [**(x1 + x2), (y1 + y2)**];

 theorem :: HAHNBAN1:7

 for x1,y1,x2,y2 be Real holds ( [**x1, y1**] * [**x2, y2**]) = [**((x1 * x2) - (y1 * y2)), ((x1 * y2) + (x2 * y1))**];

 ::$Canceled

 theorem :: HAHNBAN1:9

 for r be Real holds |. [**r, 0 **].| = |.r.|;

 theorem :: HAHNBAN1:10

 for x,y be Element of F_Complex holds ( Re (x + y)) = (( Re x) + ( Re y)) & ( Im (x + y)) = (( Im x) + ( Im y)) by COMPLEX1: 8;

 theorem :: HAHNBAN1:11

 for x,y be Element of F_Complex holds ( Re (x * y)) = ((( Re x) * ( Re y)) - (( Im x) * ( Im y))) & ( Im (x * y)) = ((( Re x) * ( Im y)) + (( Re y) * ( Im x))) by COMPLEX1: 9;

 begin

 definition

 let K be 1-sorted;

 let V be ModuleStr over K;

 mode Functional of V is Function of the carrier of V, the carrier of K;

 end

 definition

 let K be non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f,g be Functional of V;

 :: HAHNBAN1:def3

 func f + g -> Functional of V means

 : Def3: for x be Element of V holds (it . x) = ((f . x) + (g . x));

 existence

 proof

 deffunc G( Element of V) = ((f . $1) + (g . $1));

 consider F be Function of the carrier of V, the carrier of K such that

 A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

 reconsider F as Functional of V;

 take F;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of V such that

 A2: for x be Element of V holds (a . x) = ((f . x) + (g . x)) and

 A3: for x be Element of V holds (b . x) = ((f . x) + (g . x));

 now

 let x be Element of V;



 thus (a . x) = ((f . x) + (g . x)) by A2

 .= (b . x) by A3;

 end;

 hence a = b by FUNCT_2: 63;

 end;

 end

 definition

 let K be non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f be Functional of V;

 :: HAHNBAN1:def4

 func - f -> Functional of V means

 : Def4: for x be Element of V holds (it . x) = ( - (f . x));

 existence

 proof

 deffunc G( Element of V) = ( - (f . $1));

 consider F be Function of the carrier of V, the carrier of K such that

 A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

 reconsider F as Functional of V;

 take F;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of V such that

 A2: for x be Element of V holds (a . x) = ( - (f . x)) and

 A3: for x be Element of V holds (b . x) = ( - (f . x));

 now

 let x be Element of V;



 thus (a . x) = ( - (f . x)) by A2

 .= (b . x) by A3;

 end;

 hence a = b by FUNCT_2: 63;

 end;

 end

 definition

 let K be non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f,g be Functional of V;

 :: HAHNBAN1:def5

 func f - g -> Functional of V equals (f + ( - g));

 coherence ;

 end

 definition

 let K be non empty multMagma;

 let V be non empty ModuleStr over K;

 let v be Element of K;

 let f be Functional of V;

 :: HAHNBAN1:def6

 func v * f -> Functional of V means

 : Def6: for x be Element of V holds (it . x) = (v * (f . x));

 existence

 proof

 deffunc G( Element of V) = (v * (f . $1));

 consider F be Function of the carrier of V, the carrier of K such that

 A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

 reconsider F as Functional of V;

 take F;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of V such that

 A2: for x be Element of V holds (a . x) = (v * (f . x)) and

 A3: for x be Element of V holds (b . x) = (v * (f . x));

 now

 let x be Element of V;



 thus (a . x) = (v * (f . x)) by A2

 .= (b . x) by A3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 definition

 let K be non empty ZeroStr;

 let V be ModuleStr over K;

 :: HAHNBAN1:def7

 func 0Functional (V) -> Functional of V equals (( [#] V) --> ( 0. K));

 coherence ;

 end

 definition

 let K be non empty multMagma;

 let V be non empty ModuleStr over K;

 let F be Functional of V;

 :: HAHNBAN1:def8

 attr F is homogeneous means

 : Def8: for x be Vector of V, r be Scalar of V holds (F . (r * x)) = (r * (F . x));

 end

 definition

 let K be non empty ZeroStr;

 let V be non empty ModuleStr over K;

 let F be Functional of V;

 :: HAHNBAN1:def9

 attr F is 0-preserving means (F . ( 0. V)) = ( 0. K);

 end

 registration

 let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

 let V be VectSp of K;

 cluster homogeneous -> 0-preserving for Functional of V;

 coherence

 proof

 let F be Functional of V;

 assume

 A1: F is homogeneous;



 thus (F . ( 0. V)) = (F . (( 0. K) * ( 0. V))) by VECTSP_1: 14

 .= (( 0. K) * (F . ( 0. V))) by A1

 .= ( 0. K);

 end;

 end

 registration

 let K be right_zeroed non empty addLoopStr;

 let V be non empty ModuleStr over K;

 cluster ( 0Functional V) -> additive;

 coherence

 proof

 let x,y be Vector of V;



 A1: (( 0Functional V) . x) = ( 0. K) & (( 0Functional V) . y) = ( 0. K) by FUNCOP_1: 7;



 thus (( 0Functional V) . (x + y)) = ( 0. K) by FUNCOP_1: 7

 .= ((( 0Functional V) . x) + (( 0Functional V) . y)) by A1, RLVECT_1:def 4;

 end;

 end

 registration

 let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 cluster ( 0Functional V) -> homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Scalar of V;



 A1: (( 0Functional V) . x) = ( 0. K) by FUNCOP_1: 7;



 thus (( 0Functional V) . (r * x)) = ( 0. K) by FUNCOP_1: 7

 .= (r * (( 0Functional V) . x)) by A1;

 end;

 end

 registration

 let K be non empty ZeroStr;

 let V be non empty ModuleStr over K;

 cluster ( 0Functional V) -> 0-preserving;

 coherence by FUNCOP_1: 7;

 end

 registration

 let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 cluster additive homogeneous 0-preserving for Functional of V;

 existence

 proof

 take ( 0Functional V);

 thus thesis;

 end;

 end

 theorem :: HAHNBAN1:12



 Th10: for K be Abelian non empty addLoopStr holds for V be non empty ModuleStr over K holds for f,g be Functional of V holds (f + g) = (g + f)

 proof

 let K be Abelian non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f,g be Functional of V;

 now

 let x be Element of V;



 thus ((f + g) . x) = ((f . x) + (g . x)) by Def3

 .= ((g + f) . x) by Def3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:13



 Th11: for K be add-associative non empty addLoopStr holds for V be non empty ModuleStr over K holds for f,g,h be Functional of V holds ((f + g) + h) = (f + (g + h))

 proof

 let K be add-associative non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f,g,h be Functional of V;

 now

 let x be Element of V;



 thus (((f + g) + h) . x) = (((f + g) . x) + (h . x)) by Def3

 .= (((f . x) + (g . x)) + (h . x)) by Def3

 .= ((f . x) + ((g . x) + (h . x))) by RLVECT_1:def 3

 .= ((f . x) + ((g + h) . x)) by Def3

 .= ((f + (g + h)) . x) by Def3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:14

 for K be non empty ZeroStr holds for V be non empty ModuleStr over K holds for x be Element of V holds (( 0Functional V) . x) = ( 0. K) by FUNCOP_1: 7;

 theorem :: HAHNBAN1:15



 Th13: for K be right_zeroed non empty addLoopStr holds for V be non empty ModuleStr over K holds for f be Functional of V holds (f + ( 0Functional V)) = f

 proof

 let K be right_zeroed non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f be Functional of V;

 now

 let x be Element of V;



 thus ((f + ( 0Functional V)) . x) = ((f . x) + (( 0Functional V) . x)) by Def3

 .= ((f . x) + ( 0. K)) by FUNCOP_1: 7

 .= (f . x) by RLVECT_1:def 4;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:16



 Th14: for K be add-associative right_zeroed right_complementable non empty addLoopStr holds for V be non empty ModuleStr over K holds for f be Functional of V holds (f - f) = ( 0Functional V)

 proof

 let K be add-associative right_zeroed right_complementable non empty addLoopStr;

 let V be non empty ModuleStr over K;

 let f be Functional of V;

 now

 let x be Element of V;



 thus ((f - f) . x) = ((f . x) + (( - f) . x)) by Def3

 .= ((f . x) + ( - (f . x))) by Def4

 .= ( 0. K) by RLVECT_1: 5

 .= (( 0Functional V) . x) by FUNCOP_1: 7;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:17



 Th15: for K be right-distributive non empty doubleLoopStr holds for V be non empty ModuleStr over K holds for r be Element of K holds for f,g be Functional of V holds (r * (f + g)) = ((r * f) + (r * g))

 proof

 let K be right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let r be Element of K;

 let f,g be Functional of V;

 now

 let x be Element of V;



 thus ((r * (f + g)) . x) = (r * ((f + g) . x)) by Def6

 .= (r * ((f . x) + (g . x))) by Def3

 .= ((r * (f . x)) + (r * (g . x))) by VECTSP_1:def 2

 .= (((r * f) . x) + (r * (g . x))) by Def6

 .= (((r * f) . x) + ((r * g) . x)) by Def6

 .= (((r * f) + (r * g)) . x) by Def3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:18



 Th16: for K be left-distributive non empty doubleLoopStr holds for V be non empty ModuleStr over K holds for r,s be Element of K holds for f be Functional of V holds ((r + s) * f) = ((r * f) + (s * f))

 proof

 let K be left-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let r,s be Element of K;

 let f be Functional of V;

 now

 let x be Element of V;



 thus (((r + s) * f) . x) = ((r + s) * (f . x)) by Def6

 .= ((r * (f . x)) + (s * (f . x))) by VECTSP_1:def 3

 .= (((r * f) . x) + (s * (f . x))) by Def6

 .= (((r * f) . x) + ((s * f) . x)) by Def6

 .= (((r * f) + (s * f)) . x) by Def3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:19



 Th17: for K be associative non empty multMagma holds for V be non empty ModuleStr over K holds for r,s be Element of K holds for f be Functional of V holds ((r * s) * f) = (r * (s * f))

 proof

 let K be associative non empty multMagma;

 let V be non empty ModuleStr over K;

 let r,s be Element of K;

 let f be Functional of V;

 now

 let x be Element of V;



 thus (((r * s) * f) . x) = ((r * s) * (f . x)) by Def6

 .= (r * (s * (f . x))) by GROUP_1:def 3

 .= (r * ((s * f) . x)) by Def6

 .= ((r * (s * f)) . x) by Def6;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: HAHNBAN1:20



 Th18: for K be left_unital non empty doubleLoopStr holds for V be non empty ModuleStr over K holds for f be Functional of V holds (( 1. K) * f) = f

 proof

 let K be left_unital non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let f be Functional of V;

 now

 let x be Element of V;



 thus ((( 1. K) * f) . x) = (( 1. K) * (f . x)) by Def6

 .= (f . x);

 end;

 hence thesis by FUNCT_2: 63;

 end;

 registration

 let K be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let f,g be additive Functional of V;

 cluster (f + g) -> additive;

 coherence

 proof

 let x,y be Vector of V;



 thus ((f + g) . (x + y)) = ((f . (x + y)) + (g . (x + y))) by Def3

 .= (((f . x) + (f . y)) + (g . (x + y))) by VECTSP_1:def 20

 .= (((f . x) + (f . y)) + ((g . x) + (g . y))) by VECTSP_1:def 20

 .= ((f . x) + ((f . y) + ((g . x) + (g . y)))) by RLVECT_1:def 3

 .= ((f . x) + ((g . x) + ((f . y) + (g . y)))) by RLVECT_1:def 3

 .= (((f . x) + (g . x)) + ((f . y) + (g . y))) by RLVECT_1:def 3

 .= (((f + g) . x) + ((f . y) + (g . y))) by Def3

 .= (((f + g) . x) + ((f + g) . y)) by Def3;

 end;

 end

 registration

 let K be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let f be additive Functional of V;

 cluster ( - f) -> additive;

 coherence

 proof

 let x,y be Vector of V;



 thus (( - f) . (x + y)) = ( - (f . (x + y))) by Def4

 .= ( - ((f . x) + (f . y))) by VECTSP_1:def 20

 .= (( - (f . x)) + ( - (f . y))) by RLVECT_1: 31

 .= ((( - f) . x) + ( - (f . y))) by Def4

 .= ((( - f) . x) + (( - f) . y)) by Def4;

 end;

 end

 registration

 let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let v be Element of K;

 let f be additive Functional of V;

 cluster (v * f) -> additive;

 coherence

 proof

 let x,y be Vector of V;



 thus ((v * f) . (x + y)) = (v * (f . (x + y))) by Def6

 .= (v * ((f . x) + (f . y))) by VECTSP_1:def 20

 .= ((v * (f . x)) + (v * (f . y))) by VECTSP_1:def 2

 .= (((v * f) . x) + (v * (f . y))) by Def6

 .= (((v * f) . x) + ((v * f) . y)) by Def6;

 end;

 end

 registration

 let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let f,g be homogeneous Functional of V;

 cluster (f + g) -> homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Scalar of V;



 thus ((f + g) . (r * x)) = ((f . (r * x)) + (g . (r * x))) by Def3

 .= ((r * (f . x)) + (g . (r * x))) by Def8

 .= ((r * (f . x)) + (r * (g . x))) by Def8

 .= (r * ((f . x) + (g . x))) by VECTSP_1:def 2

 .= (r * ((f + g) . x)) by Def3;

 end;

 end

 registration

 let K be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let f be homogeneous Functional of V;

 cluster ( - f) -> homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Scalar of V;



 thus (( - f) . (r * x)) = ( - (f . (r * x))) by Def4

 .= ( - (r * (f . x))) by Def8

 .= (r * ( - (f . x))) by Lm1

 .= (r * (( - f) . x)) by Def4;

 end;

 end

 registration

 let K be add-associative right_zeroed right_complementable right-distributive associative commutative non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 let v be Element of K;

 let f be homogeneous Functional of V;

 cluster (v * f) -> homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Scalar of V;



 thus ((v * f) . (r * x)) = (v * (f . (r * x))) by Def6

 .= (v * (r * (f . x))) by Def8

 .= (r * (v * (f . x))) by GROUP_1:def 3

 .= (r * ((v * f) . x)) by Def6;

 end;

 end

 definition

 let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 mode linear-Functional of V is additive homogeneous Functional of V;

 end

 begin

 definition

 let K be Abelian add-associative right_zeroed right_complementable right-distributive associative commutative non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 :: HAHNBAN1:def10

 func V *' -> non empty strict ModuleStr over K means

 : Def10: (for x be set holds x in the carrier of it iff x is linear-Functional of V) & (for f,g be linear-Functional of V holds (the addF of it . (f,g)) = (f + g)) & ( 0. it ) = ( 0Functional V) & for f be linear-Functional of V holds for x be Element of K holds (the lmult of it . (x,f)) = (x * f);

 existence

 proof

 defpred P[ set, set, set] means ex f,g be Functional of V st $1 = f & $2 = g & $3 = (f + g);

 ( 0Functional V) in the set of all x where x be linear-Functional of V;

 then

 reconsider ca = the set of all x where x be linear-Functional of V as non empty set;

 A1:

 now

 let x be set;

 thus x in ca implies x is linear-Functional of V

 proof

 assume x in ca;

 then ex y be linear-Functional of V st x = y;

 hence thesis;

 end;

 thus x is linear-Functional of V implies x in ca;

 end;

 then

 reconsider 0F = ( 0Functional V) as Element of ca;



 A2: for x,y be Element of ca holds ex u be Element of ca st P[x, y, u]

 proof

 let x,y be Element of ca;

 reconsider f = x, g = y as linear-Functional of V by A1;

 reconsider u = (f + g) as Element of ca by A1;

 take u, f, g;

 thus thesis;

 end;

 consider ad be Function of [:ca, ca:], ca such that

 A3: for x,y be Element of ca holds P[x, y, (ad . (x,y))] from BINOP_1:sch 3( A2);

 defpred P[ Element of K, set, set] means ex f be Functional of V st $2 = f & $3 = ($1 * f);



 A4: for x be Element of K, y be Element of ca holds ex u be Element of ca st P[x, y, u]

 proof

 let x be Element of K, y be Element of ca;

 reconsider f = y as linear-Functional of V by A1;

 reconsider u = (x * f) as Element of ca by A1;

 take u, f;

 thus thesis;

 end;

 consider lm be Function of [:the carrier of K, ca:], ca such that

 A5: for x be Element of K, y be Element of ca holds P[x, y, (lm . (x,y))] from BINOP_1:sch 3( A4);

 A6:

 now

 let f be linear-Functional of V;

 reconsider y = f as Element of ca by A1;

 let x be Element of K;

 ex f1 be Functional of V st y = f1 & (lm . (x,y)) = (x * f1) by A5;

 hence (lm . (x,f)) = (x * f);

 end;

 reconsider V1 = ModuleStr (# ca, ad, 0F, lm #) as non empty strict ModuleStr over K;

 take V1;

 now

 let f,g be linear-Functional of V;

 reconsider x = f, y = g as Element of ca by A1;

 ex f1,g1 be Functional of V st x = f1 & y = g1 & (ad . (x,y)) = (f1 + g1) by A3;

 hence (ad . (f,g)) = (f + g);

 end;

 hence thesis by A1, A6;

 end;

 uniqueness

 proof

 let V1,V2 be non empty strict ModuleStr over K;

 assume that

 A7: for x be set holds x in the carrier of V1 iff x is linear-Functional of V and

 A8: for f,g be linear-Functional of V holds (the addF of V1 . (f,g)) = (f + g) and

 A9: ( 0. V1) = ( 0Functional V) and

 A10: for f be linear-Functional of V holds for x be Element of K holds (the lmult of V1 . (x,f)) = (x * f) and

 A11: for x be set holds x in the carrier of V2 iff x is linear-Functional of V and

 A12: for f,g be linear-Functional of V holds (the addF of V2 . (f,g)) = (f + g) and

 A13: ( 0. V2) = ( 0Functional V) and

 A14: for f be linear-Functional of V holds for x be Element of K holds (the lmult of V2 . (x,f)) = (x * f);

 A15:

 now

 let r be Element of K;

 let x be Element of V1;

 reconsider f = x as linear-Functional of V by A7;



 thus (the lmult of V1 . (r,x)) = (r * f) by A10

 .= (the lmult of V2 . (r,x)) by A14;

 end;

 now

 let x be object;

 thus x in the carrier of V1 implies x in the carrier of V2

 proof

 assume x in the carrier of V1;

 then x is linear-Functional of V by A7;

 hence thesis by A11;

 end;

 assume x in the carrier of V2;

 then x is linear-Functional of V by A11;

 hence x in the carrier of V1 by A7;

 end;

 then

 A16: the carrier of V1 = the carrier of V2 by TARSKI: 2;

 now

 let x,y be Element of V1;

 reconsider f = x, g = y as linear-Functional of V by A7;



 thus (the addF of V1 . (x,y)) = (f + g) by A8

 .= (the addF of V2 . (x,y)) by A12;

 end;

 then the addF of V1 = the addF of V2 by A16, BINOP_1: 2;

 hence thesis by A9, A13, A16, A15, BINOP_1: 2;

 end;

 end

 registration

 let K be Abelian add-associative right_zeroed right_complementable right-distributive associative commutative non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 cluster (V *' ) -> Abelian;

 coherence

 proof

 let v,w be Element of (V *' );

 reconsider f = v, g = w as linear-Functional of V by Def10;



 thus (v + w) = (f + g) by Def10

 .= (g + f) by Th10

 .= (w + v) by Def10;

 end;

 end

 registration

 let K be Abelian add-associative right_zeroed right_complementable right-distributive associative commutative non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 cluster (V *' ) -> add-associative;

 coherence

 proof

 let u,v,w be Element of (V *' );

 reconsider f = u, g = v, h = w as linear-Functional of V by Def10;



 thus ((u + v) + w) = (the addF of (V *' ) . ((f + g),w)) by Def10

 .= ((f + g) + h) by Def10

 .= (f + (g + h)) by Th11

 .= (the addF of (V *' ) . (u,(g + h))) by Def10

 .= (u + (v + w)) by Def10;

 end;

 cluster (V *' ) -> right_zeroed;

 coherence

 proof

 let x be Element of (V *' );

 reconsider f = x as linear-Functional of V by Def10;



 thus (x + ( 0. (V *' ))) = (the addF of (V *' ) . (x,( 0Functional V))) by Def10

 .= (f + ( 0Functional V)) by Def10

 .= x by Th13;

 end;

 cluster (V *' ) -> right_complementable;

 coherence

 proof

 let x be Element of (V *' );

 reconsider f = x as linear-Functional of V by Def10;

 reconsider b = ( - f) as Element of (V *' ) by Def10;

 take b;



 thus (x + b) = (f - f) by Def10

 .= ( 0Functional V) by Th14

 .= ( 0. (V *' )) by Def10;

 end;

 end

 registration

 let K be Abelian add-associative right_zeroed right_complementable left_unital distributive associative commutative non empty doubleLoopStr;

 let V be non empty ModuleStr over K;

 cluster (V *' ) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

 coherence

 proof

 now

 let x,y be Element of K;

 let v,w be Element of (V *' );

 reconsider f = v, g = w as linear-Functional of V by Def10;



 thus (x * (v + w)) = (the lmult of (V *' ) . (x,(f + g))) by Def10

 .= (x * (f + g)) by Def10

 .= ((x * f) + (x * g)) by Th15

 .= (the addF of (V *' ) . ((x * f),(x * g))) by Def10

 .= (the addF of (V *' ) . ((the lmult of (V *' ) . (x,f)),(x * g))) by Def10

 .= ((x * v) + (x * w)) by Def10;



 thus ((x + y) * v) = ((x + y) * f) by Def10

 .= ((x * f) + (y * f)) by Th16

 .= (the addF of (V *' ) . ((x * f),(y * f))) by Def10

 .= (the addF of (V *' ) . ((the lmult of (V *' ) . (x,f)),(y * f))) by Def10

 .= ((x * v) + (y * v)) by Def10;



 thus ((x * y) * v) = ((x * y) * f) by Def10

 .= (x * (y * f)) by Th17

 .= (the lmult of (V *' ) . (x,(y * f))) by Def10

 .= (x * (y * v)) by Def10;



 thus (( 1. K) * v) = (( 1. K) * f) by Def10

 .= v by Th18;

 end;

 hence thesis;

 end;

 end

 begin

 definition

 let K be 1-sorted;

 let V be ModuleStr over K;

 mode RFunctional of V is Function of the carrier of V, REAL ;

 end

 definition

 let K be 1-sorted;

 let V be non empty ModuleStr over K;

 let F be RFunctional of V;

 :: HAHNBAN1:def11

 attr F is subadditive means

 : Def11: for x,y be Vector of V holds (F . (x + y)) <= ((F . x) + (F . y));

 end

 definition

 let K be 1-sorted;

 let V be non empty ModuleStr over K;

 let F be RFunctional of V;

 :: HAHNBAN1:def12

 attr F is additive means

 : Def12: for x,y be Vector of V holds (F . (x + y)) = ((F . x) + (F . y));

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let F be RFunctional of V;

 :: HAHNBAN1:def13

 attr F is Real_homogeneous means

 : Def13: for v be Vector of V holds for r be Real holds (F . ( [**r, 0 **] * v)) = (r * (F . v));

 end

 theorem :: HAHNBAN1:21



 Th19: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex holds for F be RFunctional of V st F is Real_homogeneous holds for v be Vector of V holds for r be Real holds (F . ( [** 0 , r**] * v)) = (r * (F . ( i_FC * v)))

 proof

 let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex ;

 let F be RFunctional of V;

 assume

 A1: F is Real_homogeneous;

 let v be Vector of V;

 let r be Real;



 thus (F . ( [** 0 , r**] * v)) = (F . (( [**r, 0 **] * i_FC ) * v))

 .= (F . ( [**r, 0 **] * ( i_FC * v))) by VECTSP_1:def 16

 .= (r * (F . ( i_FC * v))) by A1;

 end;

 definition

 let V be non empty ModuleStr over F_Complex ;

 let F be RFunctional of V;

 :: HAHNBAN1:def14

 attr F is homogeneous means

 : Def14: for v be Vector of V holds for r be Scalar of V holds (F . (r * v)) = ( |.r.| * (F . v));

 end

 definition

 let K be 1-sorted;

 let V be ModuleStr over K;

 let F be RFunctional of V;

 :: HAHNBAN1:def15

 attr F is 0-preserving means (F . ( 0. V)) = 0 ;

 end

 registration

 let K be 1-sorted;

 let V be non empty ModuleStr over K;

 cluster additive -> subadditive for RFunctional of V;

 coherence ;

 end

 registration

 let V be VectSp of F_Complex ;

 cluster Real_homogeneous -> 0-preserving for RFunctional of V;

 coherence

 proof

 let F be RFunctional of V;

 assume

 A1: F is Real_homogeneous;



 A2: ( 0. F_Complex ) = [** 0 , 0 **] by COMPLFLD: 7;



 thus (F . ( 0. V)) = (F . (( 0. F_Complex ) * ( 0. V))) by VECTSP_1: 14

 .= ( 0 * (F . ( 0. V))) by A1, A2

 .= 0 ;

 end;

 end

 definition

 let K be 1-sorted;

 let V be ModuleStr over K;

 :: HAHNBAN1:def16

 func 0RFunctional (V) -> RFunctional of V equals (( [#] V) --> 0 );

 coherence

 proof

 (( [#] V) --> ( In ( 0 , REAL ))) is RFunctional of V;

 hence thesis;

 end;

 end

 registration

 let K be 1-sorted;

 let V be non empty ModuleStr over K;

 cluster ( 0RFunctional V) -> additive;

 coherence

 proof

 let x,y be Vector of V;

 (( 0RFunctional V) . x) = 0 & (( 0RFunctional V) . y) = 0 by FUNCOP_1: 7;

 hence thesis by FUNCOP_1: 7;

 end;

 cluster ( 0RFunctional V) -> 0-preserving;

 coherence by FUNCOP_1: 7;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster ( 0RFunctional V) -> Real_homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Real;

 (( 0RFunctional V) . x) = 0 by FUNCOP_1: 7;

 hence thesis by FUNCOP_1: 7;

 end;

 cluster ( 0RFunctional V) -> homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Scalar of V;

 (( 0RFunctional V) . x) = 0 by FUNCOP_1: 7;

 hence thesis by FUNCOP_1: 7;

 end;

 end

 registration

 let K be 1-sorted;

 let V be non empty ModuleStr over K;

 cluster additive 0-preserving for RFunctional of V;

 existence

 proof

 take ( 0RFunctional V);

 thus thesis;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster additive Real_homogeneous homogeneous for RFunctional of V;

 existence

 proof

 take ( 0RFunctional V);

 thus thesis;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 mode Semi-Norm of V is subadditive homogeneous RFunctional of V;

 end

 begin

 definition

 let V be non empty ModuleStr over F_Complex ;

 :: HAHNBAN1:def17

 func RealVS (V) -> strict RLSStruct means

 : Def17: the addLoopStr of it = the addLoopStr of V & for r be Real, v be Vector of V holds (the Mult of it . (r,v)) = ( [**r, 0 **] * v);

 existence

 proof

 deffunc F( Element of REAL , Element of V) = ( [**$1, 0 **] * $2);

 consider f be Function of [: REAL , the carrier of V:], the carrier of V such that

 A1: for r be Element of REAL , v be Vector of V holds (f . (r,v)) = F(r,v) from BINOP_1:sch 4;

 take R = RLSStruct (# the carrier of V, ( 0. V), the addF of V, f #);

 thus the addLoopStr of R = the addLoopStr of V;

 let r be Real;

 let v be Vector of V;

 reconsider r as Element of REAL by XREAL_0:def 1;

 (f . (r,v)) = F(r,v) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let a,b be strict RLSStruct such that

 A2: the addLoopStr of a = the addLoopStr of V and

 A3: for r be Real, v be Vector of V holds (the Mult of a . (r,v)) = ( [**r, 0 **] * v) and

 A4: the addLoopStr of b = the addLoopStr of V and

 A5: for r be Real, v be Vector of V holds (the Mult of b . (r,v)) = ( [**r, 0 **] * v);

 now

 let r be Element of REAL , v be Vector of V;



 thus (the Mult of a . (r,v)) = ( [**r, 0 **] * v) by A3

 .= (the Mult of b . (r,v)) by A5;

 end;

 hence thesis by A2, A4, BINOP_1: 2;

 end;

 end

 registration

 let V be non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> non empty;

 coherence

 proof

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 hence thesis;

 end;

 end

 registration

 let V be Abelian non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> Abelian;

 coherence

 proof

 let v,w be Element of ( RealVS V);



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v, w1 = w as Element of V;



 thus (v + w) = (v1 + w1) by A1

 .= (w1 + v1)

 .= (w + v) by A1;

 end;

 end

 registration

 let V be add-associative non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> add-associative;

 coherence

 proof

 let u,v,w be Element of ( RealVS V);



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider u1 = u, v1 = v, w1 = w as Element of V;



 thus ((u + v) + w) = ((u1 + v1) + w1) by A1

 .= (u1 + (v1 + w1)) by RLVECT_1:def 3

 .= (u + (v + w)) by A1;

 end;

 end

 registration

 let V be right_zeroed non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> right_zeroed;

 coherence

 proof

 let v be Element of ( RealVS V);



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v as Element of V;



 thus (v + ( 0. ( RealVS V))) = (v1 + ( 0. V)) by A1

 .= v by RLVECT_1:def 4;

 end;

 end

 registration

 let V be right_complementable non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> right_complementable;

 coherence

 proof

 let v be Element of ( RealVS V);



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v as Element of V;

 consider w1 be Element of V such that

 A2: (v1 + w1) = ( 0. V) by ALGSTR_0:def 11;

 reconsider w = w1 as Element of ( RealVS V) by A1;

 take w;

 thus thesis by A1, A2;

 end;

 end

 registration

 let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F_Complex ;

 cluster ( RealVS V) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

 coherence

 proof

 thus for a be Real holds for v,w be Element of ( RealVS V) holds (a * (v + w)) = ((a * v) + (a * w))

 proof

 let a be Real;

 reconsider a as Real;

 let v,w be Element of ( RealVS V);

 set a1 = [**a, 0 **];



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v, w1 = w as Element of V;

 (a * (v + w)) = ( [**a, 0 **] * (v1 + w1)) by A1, Def17

 .= ((a1 * v1) + (a1 * w1)) by VECTSP_1:def 14

 .= (the addF of V . [(the Mult of ( RealVS V) . (a,v1)), ( [**a, 0 **] * w1)]) by Def17

 .= ((a * v) + (a * w)) by A1, Def17;

 hence thesis;

 end;

 thus for a,b be Real holds for v be Element of ( RealVS V) holds ((a + b) * v) = ((a * v) + (b * v))

 proof

 let a,b be Real;

 reconsider a, b as Real;

 let v be Element of ( RealVS V);

 set a1 = [**a, 0 **];

 set b1 = [**b, 0 **];



 A2: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v as Element of V;

 ( [**a, 0 **] + [**b, 0 **]) = [**(a + b), 0 **];



 then ((a + b) * v) = (( [**a, 0 **] + [**b, 0 **]) * v1) by Def17

 .= ((a1 * v1) + (b1 * v1)) by VECTSP_1:def 15

 .= (the addF of ( RealVS V) . [(the Mult of ( RealVS V) . (a,v)), ( [**b, 0 **] * v1)]) by A2, Def17

 .= ((a * v) + (b * v)) by Def17;

 hence thesis;

 end;

 thus for a,b be Real holds for v be Element of ( RealVS V) holds ((a * b) * v) = (a * (b * v))

 proof

 let a,b be Real;

 reconsider a, b as Real;

 let v be Element of ( RealVS V);

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v as Element of V;

 [**(a * b), 0 **] = ( [**a, 0 **] * [**b, 0 **]);



 then ((a * b) * v) = (( [**a, 0 **] * [**b, 0 **]) * v1) by Def17

 .= ( [**a, 0 **] * ( [**b, 0 **] * v1)) by VECTSP_1:def 16

 .= (the Mult of ( RealVS V) . (a,( [**b, 0 **] * v1))) by Def17

 .= (a * (b * v)) by Def17;

 hence thesis;

 end;

 let v be Element of ( RealVS V);

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider v1 = v as Element of V;



 thus (1 * v) = ( [**1, 0 **] * v1) by Def17

 .= v by COMPLFLD: 8, VECTSP_1:def 17;

 end;

 end

 theorem :: HAHNBAN1:22



 Th20: for V be non empty VectSp of F_Complex holds for M be Subspace of V holds ( RealVS M) is Subspace of ( RealVS V)

 proof

 let V be non empty VectSp of F_Complex ;

 let M be Subspace of V;



 A1: the carrier of M c= the carrier of V by VECTSP_4:def 2;



 A2: the lmult of M = (the lmult of V | [:the carrier of F_Complex , the carrier of M:]) by VECTSP_4:def 2;



 A3: the addLoopStr of M = the addLoopStr of ( RealVS M) by Def17;



 A4: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 hence

 A5: the carrier of ( RealVS M) c= the carrier of ( RealVS V) by A3, VECTSP_4:def 2;

 then [: REAL , the carrier of ( RealVS M):] c= [: REAL , the carrier of ( RealVS V):] by ZFMISC_1: 95;

 then [: REAL , the carrier of ( RealVS M):] c= ( dom the Mult of ( RealVS V)) by FUNCT_2:def 1;

 then

 A6: ( dom (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):])) = [: REAL , the carrier of ( RealVS M):] by RELAT_1: 62;

 ( rng (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):])) c= the carrier of ( RealVS M)

 proof

 let y be object;

 assume y in ( rng (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):]));

 then

 consider x be object such that

 A7: x in ( dom (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):])) and

 A8: y = ((the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):]) . x) by FUNCT_1:def 3;

 consider a,b be object such that

 A9: x = [a, b] by A7, RELAT_1:def 1;

 reconsider a as Element of REAL by A7, A9, ZFMISC_1: 87;

 reconsider b as Element of ( RealVS M) by A6, A7, A9, ZFMISC_1: 87;

 reconsider b1 = b as Element of M by A3;

 reconsider b2 = b1 as Element of V by A1;

 [ [**a, 0 **], b2] in [:the carrier of F_Complex , the carrier of V:] by ZFMISC_1: 87;

 then [ [**a, 0 **], b1] in [:the carrier of F_Complex , the carrier of M:] & [ [**a, 0 **], b2] in ( dom the lmult of V) by FUNCT_2:def 1, ZFMISC_1: 87;

 then [ [**a, 0 **], b2] in (( dom the lmult of V) /\ [:the carrier of F_Complex , the carrier of M:]) by XBOOLE_0:def 4;

 then

 A10: [ [**a, 0 **], b2] in ( dom (the lmult of V | [:the carrier of F_Complex , the carrier of M:])) by RELAT_1: 61;

 y = (the Mult of ( RealVS V) . (a,b)) by A7, A8, A9, FUNCT_1: 47

 .= ( [**a, 0 **] * b2) by Def17

 .= ( [**a, 0 **] * b1) by A2, A10, FUNCT_1: 47

 .= (the Mult of ( RealVS M) . (a,b)) by Def17;

 hence thesis;

 end;

 then

 reconsider RM = (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):]) as Function of [: REAL , the carrier of ( RealVS M):], the carrier of ( RealVS M) by A6, FUNCT_2: 2;



 thus ( 0. ( RealVS M)) = ( 0. M) by A3

 .= ( 0. V) by VECTSP_4:def 2

 .= ( 0. ( RealVS V)) by A4;

 thus the addF of ( RealVS M) = (the addF of ( RealVS V) || the carrier of ( RealVS M)) by A3, A4, VECTSP_4:def 2;

 now

 let a be Element of REAL , b be Element of ( RealVS M);

 reconsider b1 = b as Element of M by A3;

 reconsider b2 = b1 as Element of V by A1;

 [ [**a, 0 **], b2] in [:the carrier of F_Complex , the carrier of V:] by ZFMISC_1: 87;

 then [ [**a, 0 **], b1] in [:the carrier of F_Complex , the carrier of M:] & [ [**a, 0 **], b2] in ( dom the lmult of V) by FUNCT_2:def 1, ZFMISC_1: 87;

 then [ [**a, 0 **], b2] in (( dom the lmult of V) /\ [:the carrier of F_Complex , the carrier of M:]) by XBOOLE_0:def 4;

 then

 A11: [ [**a, 0 **], b2] in ( dom (the lmult of V | [:the carrier of F_Complex , the carrier of M:])) by RELAT_1: 61;

 a in REAL & b in the carrier of ( RealVS V) by A5;

 then [a, b] in [: REAL , the carrier of ( RealVS V):] by ZFMISC_1: 87;

 then [a, b] in [: REAL , the carrier of ( RealVS M):] & [a, b] in ( dom the Mult of ( RealVS V)) by FUNCT_2:def 1, ZFMISC_1: 87;

 then [a, b] in (( dom the Mult of ( RealVS V)) /\ [: REAL , the carrier of ( RealVS M):]) by XBOOLE_0:def 4;

 then

 A12: [a, b] in ( dom RM) by RELAT_1: 61;



 thus (the Mult of ( RealVS M) . (a,b)) = ( [**a, 0 **] * b1) by Def17

 .= ( [**a, 0 **] * b2) by A2, A11, FUNCT_1: 47

 .= (the Mult of ( RealVS V) . (a,b)) by Def17

 .= (RM . (a,b)) by A12, FUNCT_1: 47;

 end;

 hence the Mult of ( RealVS M) = (the Mult of ( RealVS V) | [: REAL , the carrier of ( RealVS M):]) by BINOP_1: 2;

 end;

 theorem :: HAHNBAN1:23



 Th21: for V be non empty ModuleStr over F_Complex holds for p be RFunctional of V holds p is Functional of ( RealVS V)

 proof

 let V be non empty ModuleStr over F_Complex ;

 let p be RFunctional of V;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 hence thesis;

 end;

 theorem :: HAHNBAN1:24



 Th22: for V be non empty VectSp of F_Complex holds for p be Semi-Norm of V holds p is Banach-Functional of ( RealVS V)

 proof

 let V be non empty VectSp of F_Complex ;

 let p be Semi-Norm of V;

 reconsider p1 = p as Functional of ( RealVS V) by Th21;



 A1: p1 is positively_homogeneous

 proof

 let x be VECTOR of ( RealVS V);

 let r be Real;

 assume

 A2: r > 0 ;

 the addLoopStr of V = the addLoopStr 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;

 end;

 p1 is subadditive

 proof

 let x,y be VECTOR of ( RealVS V);



 A3: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x, y1 = y as Vector of V;

 (x + y) = (x1 + y1) by A3;

 hence thesis by Def11;

 end;

 hence thesis by A1;

 end;

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be Functional of V;

 :: HAHNBAN1:def18

 func projRe (l) -> Functional of ( RealVS V) means

 : Def18: for i be Element of V holds (it . i) = ( Re (l . i));

 existence

 proof

 deffunc F( Element of V) = ( Re (l . $1));

 consider f be Function of the carrier of V, REAL such that

 A1: for i be Element of V holds (f . i) = F(i) from FUNCT_2:sch 4;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider f as Functional of ( RealVS V);

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of ( RealVS V);

 assume

 A2: for i be Element of V holds (a . i) = ( Re (l . i));

 assume

 A3: for i be Element of V holds (b . i) = ( Re (l . i));

 now

 let i be Element of ( RealVS V);

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider j = i as Element of V;



 thus (a . i) = ( Re (l . j)) by A2

 .= (b . i) by A3;

 end;

 hence a = b by FUNCT_2: 63;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be Functional of V;

 :: HAHNBAN1:def19

 func projIm (l) -> Functional of ( RealVS V) means

 : Def19: for i be Element of V holds (it . i) = ( Im (l . i));

 existence

 proof

 deffunc F( Element of V) = ( Im (l . $1));

 consider f be Function of the carrier of V, REAL such that

 A1: for i be Element of V holds (f . i) = F(i) from FUNCT_2:sch 4;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider f as Functional of ( RealVS V);

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of ( RealVS V);

 assume

 A2: for i be Element of V holds (a . i) = ( Im (l . i));

 assume

 A3: for i be Element of V holds (b . i) = ( Im (l . i));

 now

 let i be Element of ( RealVS V);

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider j = i as Element of V;



 thus (a . i) = ( Im (l . j)) by A2

 .= (b . i) by A3;

 end;

 hence a = b by FUNCT_2: 63;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be Functional of ( RealVS V);

 :: HAHNBAN1:def20

 func RtoC (l) -> RFunctional of V equals l;

 coherence

 proof

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 hence thesis;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be RFunctional of V;

 :: HAHNBAN1:def21

 func CtoR (l) -> Functional of ( RealVS V) equals l;

 coherence

 proof

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 hence thesis;

 end;

 end

 registration

 let V be non empty VectSp of F_Complex ;

 let l be additive Functional of ( RealVS V);

 cluster ( RtoC l) -> additive;

 coherence

 proof

 let x,y be Vector of V;



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x, y1 = y as VECTOR of ( RealVS V);

 (x + y) = (x1 + y1) by A1;

 hence (( RtoC l) . (x + y)) = ((( RtoC l) . x) + (( RtoC l) . y)) by HAHNBAN:def 2;

 end;

 end

 registration

 let V be non empty VectSp of F_Complex ;

 let l be additive RFunctional of V;

 cluster ( CtoR l) -> additive;

 coherence

 proof

 let x,y be VECTOR of ( RealVS V);



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x, y1 = y as Vector of V;

 (x + y) = (x1 + y1) by A1;

 hence thesis by Def12;

 end;

 end

 registration

 let V be non empty VectSp of F_Complex ;

 let l be homogeneous Functional of ( RealVS V);

 cluster ( RtoC l) -> Real_homogeneous;

 coherence

 proof

 let x be Vector of V;

 let r be Real;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x as VECTOR of ( RealVS V);

 ( [**r, 0 **] * x) = (r * x1) by Def17;

 hence thesis by HAHNBAN:def 3;

 end;

 end

 registration

 let V be non empty VectSp of F_Complex ;

 let l be Real_homogeneous RFunctional of V;

 cluster ( CtoR l) -> homogeneous;

 coherence

 proof

 let x be VECTOR of ( RealVS V);

 let r be Real;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x as Vector of V;

 reconsider r as Real;

 ( [**r, 0 **] * x1) = (r * x) by Def17;

 hence thesis by Def13;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be RFunctional of V;

 :: HAHNBAN1:def22

 func i-shift (l) -> RFunctional of V means

 : Def22: for v be Element of V holds (it . v) = (l . ( i_FC * v));

 existence

 proof

 deffunc F( Element of V) = (l . ( i_FC * $1));

 consider f be Function of the carrier of V, REAL such that

 A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

 reconsider f as RFunctional of V;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let F1,F2 be RFunctional of V such that

 A2: for v be Element of V holds (F1 . v) = (l . ( i_FC * v)) and

 A3: for v be Element of V holds (F2 . v) = (l . ( i_FC * v));

 now

 let v be Element of V;



 thus (F1 . v) = (l . ( i_FC * v)) by A2

 .= (F2 . v) by A3;

 end;

 hence F1 = F2 by FUNCT_2: 63;

 end;

 end

 definition

 let V be non empty ModuleStr over F_Complex ;

 let l be Functional of ( RealVS V);

 :: HAHNBAN1:def23

 func prodReIm (l) -> Functional of V means

 : Def23: for v be Element of V holds (it . v) = [**(( RtoC l) . v), ( - (( i-shift ( RtoC l)) . v))**];

 existence

 proof

 deffunc F( Element of V) = [**(( RtoC l) . $1), ( - (( i-shift ( RtoC l)) . $1))**];

 consider f be Function of the carrier of V, the carrier of F_Complex such that

 A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

 reconsider f as Functional of V;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let a,b be Functional of V;

 assume

 A2: for v be Element of V holds (a . v) = [**(( RtoC l) . v), ( - (( i-shift ( RtoC l)) . v))**];

 assume

 A3: for v be Element of V holds (b . v) = [**(( RtoC l) . v), ( - (( i-shift ( RtoC l)) . v))**];

 now

 let v be Element of V;



 thus (a . v) = [**(( RtoC l) . v), ( - (( i-shift ( RtoC l)) . v))**] by A2

 .= (b . v) by A3;

 end;

 hence a = b by FUNCT_2: 63;

 end;

 end

 theorem :: HAHNBAN1:25



 Th23: for V be non empty VectSp of F_Complex holds for l be linear-Functional of V holds ( projRe l) is linear-Functional of ( RealVS V)

 proof

 let V be non empty VectSp of F_Complex ;

 let l be linear-Functional of V;



 A1: ( projRe l) is homogeneous

 proof

 let x be VECTOR of ( RealVS V);

 let r be Real;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x as Vector of V;

 (r * x) = ( [**r, 0 **] * x1) by Def17;



 hence (( projRe l) . (r * x)) = ( Re (l . ( [**r, 0 **] * x1))) by Def18

 .= ( Re ( [**r, 0 **] * (l . x1))) by Def8

 .= ((( Re [**r, 0 **]) * ( Re (l . x1))) - (( Im [**r, 0 **]) * ( Im (l . x1)))) by COMPLEX1: 9

 .= ((( Re [**r, 0 **]) * ( Re (l . x1))) - ( 0 * ( Im (l . x1)))) by COMPLEX1: 12

 .= (r * ( Re (l . x1))) by COMPLEX1: 12

 .= (r * (( projRe l) . x)) by Def18;

 end;

 ( projRe l) is additive

 proof

 let x,y be VECTOR of ( RealVS V);



 A2: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x, y1 = y as Vector of V;



 thus (( projRe l) . (x + y)) = ( Re (l . (x1 + y1))) by A2, Def18

 .= ( Re ((l . x1) + (l . y1))) by VECTSP_1:def 20

 .= (( Re (l . x1)) + ( Re (l . y1))) by COMPLEX1: 8

 .= (( Re (l . x1)) + (( projRe l) . y)) by Def18

 .= ((( projRe l) . x) + (( projRe l) . y)) by Def18;

 end;

 hence thesis by A1;

 end;

 theorem :: HAHNBAN1:26

 for V be non empty VectSp of F_Complex holds for l be linear-Functional of V holds ( projIm l) is linear-Functional of ( RealVS V)

 proof

 let V be non empty VectSp of F_Complex ;

 let l be linear-Functional of V;



 A1: ( projIm l) is homogeneous

 proof

 let x be VECTOR of ( RealVS V);

 let r be Real;

 the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x as Vector of V;

 (r * x) = ( [**r, 0 **] * x1) by Def17;



 hence (( projIm l) . (r * x)) = ( Im (l . ( [**r, 0 **] * x1))) by Def19

 .= ( Im ( [**r, 0 **] * (l . x1))) by Def8

 .= ((( Re [**r, 0 **]) * ( Im (l . x1))) + (( Re (l . x1)) * ( Im [**r, 0 **]))) by COMPLEX1: 9

 .= ((( Re [**r, 0 **]) * ( Im (l . x1))) + (( Re (l . x1)) * 0 )) by COMPLEX1: 12

 .= (r * ( Im (l . x1))) by COMPLEX1: 12

 .= (r * (( projIm l) . x)) by Def19;

 end;

 ( projIm l) is additive

 proof

 let x,y be VECTOR of ( RealVS V);



 A2: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;

 then

 reconsider x1 = x, y1 = y as Vector of V;



 thus (( projIm l) . (x + y)) = ( Im (l . (x1 + y1))) by A2, Def19

 .= ( Im ((l . x1) + (l . y1))) by VECTSP_1:def 20

 .= (( Im (l . x1)) + ( Im (l . y1))) by COMPLEX1: 8

 .= (( Im (l . x1)) + (( projIm l) . y)) by Def19

 .= ((( projIm l) . x) + (( projIm l) . y)) by Def19;

 end;

 hence thesis by A1;

 end;

 theorem :: HAHNBAN1:27



 Th25: for V be non empty VectSp of F_Complex holds for l be linear-Functional of ( RealVS V) holds ( prodReIm l) is linear-Functional of V

 proof

 let V be non empty VectSp of F_Complex ;

 let l be linear-Functional of ( RealVS V);



 A1: ( prodReIm l) is homogeneous

 proof

 let x be Vector of V;

 let r be Scalar of V;

 reconsider r1 = r as Element of COMPLEX by COMPLFLD:def 1;

 set a = ( Re r1), b = ( Im r1);



 A2: r1 = (a + (b * )) by COMPLEX1: 13;



 A3: ( - ( 1_ F_Complex )) = [**( - 1), 0 **] by COMPLFLD: 2, COMPLFLD: 8;

 x = (( i_FC * ( i_FC * ( - ( 1_ F_Complex )))) * x) by Th3, Th4, VECTSP_1:def 17

 .= ( i_FC * ((( - ( 1_ F_Complex )) * i_FC ) * x)) by VECTSP_1:def 16;



 then

 A4: ((a * ( - (( RtoC l) . ( i_FC * x)))) + ((( RtoC l) . x) * b)) = (( - (a * (( RtoC l) . ( i_FC * x)))) + (b * (( RtoC l) . ( i_FC * ((( - ( 1_ F_Complex )) * i_FC ) * x)))))

 .= (( - (( RtoC l) . ( [**a, 0 **] * ( i_FC * x)))) + ( - (( - b) * (( RtoC l) . ( i_FC * ((( - ( 1_ F_Complex )) * i_FC ) * x)))))) by Def13

 .= (( - (( RtoC l) . ( [**a, 0 **] * ( i_FC * x)))) + ( - (( RtoC l) . ( [** 0 , ( - b)**] * ((( - ( 1_ F_Complex )) * i_FC ) * x))))) by Th19

 .= (( - (( RtoC l) . ( [**a, 0 **] * ( i_FC * x)))) + ( - (( RtoC l) . ( [** 0 , ( - b)**] * (( - ( 1_ F_Complex )) * ( i_FC * x)))))) by VECTSP_1:def 16

 .= (( - (( RtoC l) . ( [**a, 0 **] * ( i_FC * x)))) + ( - (( RtoC l) . (( [** 0 , ( - b)**] * ( - ( 1_ F_Complex ))) * ( i_FC * x))))) by VECTSP_1:def 16

 .= ( - ((( RtoC l) . ( [**a, 0 **] * ( i_FC * x))) + (( RtoC l) . ( [** 0 , b**] * ( i_FC * x))))) by A3

 .= ( - (( RtoC l) . (( [**a, 0 **] * ( i_FC * x)) + ( [** 0 , b**] * ( i_FC * x))))) by Def12

 .= ( - (( RtoC l) . (( [**a, 0 **] + [** 0 , b**]) * ( i_FC * x)))) by VECTSP_1:def 15

 .= ( - (( RtoC l) . (( i_FC * r) * x))) by A2, VECTSP_1:def 16;



 A5: ((a * (( RtoC l) . x)) - (b * ( - (( RtoC l) . ( i_FC * x))))) = ((a * (( RtoC l) . x)) + (b * (( RtoC l) . ( i_FC * x))))

 .= ((( RtoC l) . ( [**a, 0 **] * x)) + (b * (( RtoC l) . ( i_FC * x)))) by Def13

 .= ((( RtoC l) . ( [**a, 0 **] * x)) + (( RtoC l) . ( [** 0 , b**] * x))) by Th19

 .= (( RtoC l) . (( [**a, 0 **] * x) + ( [** 0 , b**] * x))) by Def12

 .= (( RtoC l) . (( [**a, 0 **] + [** 0 , b**]) * x)) by VECTSP_1:def 15

 .= (( RtoC l) . (r * x)) by COMPLEX1: 13;



 thus (( prodReIm l) . (r * x)) = [**(( RtoC l) . (r * x)), ( - (( i-shift ( RtoC l)) . (r * x)))**] by Def23

 .= [**(( RtoC l) . (r * x)), ( - (( RtoC l) . ( i_FC * (r * x))))**] by Def22

 .= ((( RtoC l) . (r * x)) + (((a * ( - (( RtoC l) . ( i_FC * x)))) + ((( RtoC l) . x) * b)) * )) by A4, VECTSP_1:def 16

 .= (r * [**(( RtoC l) . x), ( - (( RtoC l) . ( i_FC * x)))**]) by A2, A5

 .= (r * [**(( RtoC l) . x), ( - (( i-shift ( RtoC l)) . x))**]) by Def22

 .= (r * (( prodReIm l) . x)) by Def23;

 end;

 ( prodReIm l) is additive

 proof

 let x,y be Vector of V;



 thus (( prodReIm l) . (x + y)) = [**(( RtoC l) . (x + y)), ( - (( i-shift ( RtoC l)) . (x + y)))**] by Def23

 .= [**(( RtoC l) . (x + y)), ( - (( RtoC l) . ( i_FC * (x + y))))**] by Def22

 .= [**((( RtoC l) . x) + (( RtoC l) . y)), ( - (( RtoC l) . ( i_FC * (x + y))))**] by Def12

 .= [**((( RtoC l) . x) + (( RtoC l) . y)), ( - (( RtoC l) . (( i_FC * x) + ( i_FC * y))))**] by VECTSP_1:def 14

 .= [**((( RtoC l) . x) + (( RtoC l) . y)), ( - ((( RtoC l) . ( i_FC * x)) + (( RtoC l) . ( i_FC * y))))**] by Def12

 .= ( [**(( RtoC l) . x), ( - (( RtoC l) . ( i_FC * x)))**] + [**(( RtoC l) . y), ( - (( RtoC l) . ( i_FC * y)))**])

 .= ( [**(( RtoC l) . x), ( - (( i-shift ( RtoC l)) . x))**] + [**(( RtoC l) . y), ( - (( RtoC l) . ( i_FC * y)))**]) by Def22

 .= ( [**(( RtoC l) . x), ( - (( i-shift ( RtoC l)) . x))**] + [**(( RtoC l) . y), ( - (( i-shift ( RtoC l)) . y))**]) by Def22

 .= ((( prodReIm l) . x) + [**(( RtoC l) . y), ( - (( i-shift ( RtoC l)) . y))**]) by Def23

 .= ((( prodReIm l) . x) + (( prodReIm l) . y)) by Def23;

 end;

 hence thesis by A1;

 end;

 ::$Notion-Name

 theorem :: HAHNBAN1:28

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

 proof

 let V be non empty VectSp of F_Complex ;

 let p be Semi-Norm of V;

 reconsider p1 = p as Banach-Functional of ( RealVS V) by Th22;

 let M be Subspace of V;

 reconsider tcM = the carrier of M as Subset of V by VECTSP_4:def 2;

 reconsider RVSM = ( RealVS M) as Subspace of ( RealVS V) by Th20;

 let l be linear-Functional of M;

 reconsider prRl = ( projRe l) as linear-Functional of RVSM by Th23;



 A1: the addLoopStr of V = the addLoopStr of ( RealVS V) by Def17;



 A2: the addLoopStr of M = the addLoopStr of ( RealVS M) by Def17;

 assume

 A3: for e be Vector of M holds for v be Vector of V st v = e holds |.(l . e).| <= (p . v);

 for x be VECTOR of RVSM holds for v be VECTOR of ( RealVS V) st x = v holds (prRl . x) <= (p1 . v)

 proof

 let x be VECTOR of RVSM;

 reconsider x1 = x as Vector of M by A2;

 let v be VECTOR of ( RealVS V);

 reconsider v1 = v as Vector of V by A1;

 (prRl . x) = ( Re (l . x1)) by Def18;

 then

 A4: (prRl . x) <= |.(l . x1).| by COMPLEX1: 54;

 assume x = v;

 then |.(l . x1).| <= (p . v1) by A3;

 hence thesis by A4, XXREAL_0: 2;

 end;

 then

 consider L1 be linear-Functional of ( RealVS V) such that

 A5: (L1 | the carrier of RVSM) = prRl and

 A6: for e be VECTOR of ( RealVS V) holds (L1 . e) <= (p1 . e) by HAHNBAN: 22;

 reconsider L = ( prodReIm L1) as linear-Functional of V by Th25;

 take L;

 now

 let x be Element of M;

 the carrier of M c= the carrier of V by VECTSP_4:def 2;

 then

 reconsider x2 = x as Element of V;

 reconsider x1 = x2, ix1 = ( i_FC * x2) as Element of ( RealVS V) by A1;

 reconsider lx = (l . x) as Element of COMPLEX by COMPLFLD:def 1;

 lx = (( Re lx) + (( Im lx) * )) by COMPLEX1: 13;

 then

 A7: ( i_FC * (l . x)) = ((( 0 * ( Re lx)) - (1 * ( Im lx))) + ((( 0 * ( Im lx)) + (1 * ( Re lx))) * ));



 A8: ( i_FC * x) = ( i_FC * x2) by VECTSP_4: 14;



 then

 A9: (L1 . ix1) = (( projRe l) . ix1) by A2, A5, FUNCT_1: 49

 .= ( Re (l . ( i_FC * x))) by A8, Def18

 .= ( Re (( - ( Im lx)) + (( Re lx) * ))) by A7, Def8

 .= ( - ( Im (l . x))) by COMPLEX1: 12;



 A10: (L1 . x1) = (( projRe l) . x1) by A2, A5, FUNCT_1: 49

 .= ( Re (l . x)) by Def18;



 thus ((L | tcM) . x) = (L . x) by FUNCT_1: 49

 .= [**(( RtoC L1) . x2), ( - (( i-shift ( RtoC L1)) . x2))**] by Def23

 .= [**( Re (l . x)), ( - (( RtoC L1) . ( i_FC * x2)))**] by A10, Def22

 .= (l . x) by A9, COMPLEX1: 13;

 end;

 hence (L | the carrier of M) = l by FUNCT_2: 63;

 let e be Vector of V;

 reconsider Le = (L . e) as Element of COMPLEX by COMPLFLD:def 1;

 ((Le *' ) / |.Le.|) in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider Ledz = ((Le *' ) / |.Le.|) as Element of F_Complex by COMPLFLD:def 1;

 reconsider e1 = e, Ledze = (Ledz * e) as VECTOR of ( RealVS V) by A1;

 per cases ;

 suppose

 A11: |.Le.| <> 0 ;



 A12: |.Ledz.| = ( |.(Le *' ).| / |. |.Le.|.|) by COMPLEX1: 67

 .= ( |.Le.| / |.Le.|) by COMPLEX1: 53

 .= 1 by A11, XCMPLX_1: 60;

 ( |.Le.| + ( 0 * )) = (Ledz * (L . e)) by Th2

 .= (L . (Ledz * e)) by Def8

 .= [**(( RtoC L1) . (Ledz * e)), ( - (( i-shift ( RtoC L1)) . (Ledz * e)))**] by Def23

 .= ((L1 . Ledze) + (( - (( i-shift ( RtoC L1)) . (Ledz * e))) * ));

 then

 A13: (L1 . Ledze) = |.(L . e).| by COMPLEX1: 77;

 (p1 . Ledze) = ( |.Ledz.| * (p . e)) by Def14

 .= (p . e) by A12;

 hence thesis by A6, A13;

 end;

 suppose

 A14: |.Le.| = 0 ;

 |.(L . e).| = |. [**(( RtoC L1) . e), ( - (( i-shift ( RtoC L1)) . e))**].| by Def23

 .= |.((( RtoC L1) . e) + (( - (( i-shift ( RtoC L1)) . e)) * )).|;

 then ((( RtoC L1) . e) + (( - (( i-shift ( RtoC L1)) . e)) * )) = ( 0 + ( 0 * )) by A14, COMPLEX1: 45;

 then (L1 . e1) = 0 by COMPLEX1: 77;

 hence thesis by A6, A14;

 end;

 end;

 begin

 theorem :: HAHNBAN1:29

 for x be Real st x > 0 holds for n be Nat holds (( power F_Complex ) . ( [**x, 0 **],n)) = [**(x to_power n), 0 **]

 proof

 let x be Real;

 defpred P[ Nat] means (( power F_Complex ) . ( [**x, 0 **],$1)) = [**(x to_power $1), 0 **];

 assume

 A1: x > 0 ;

 A2:

 now

 let n be Nat;

 assume P[n];



 then (( power F_Complex ) . ( [**x, 0 **],(n + 1))) = ( [**(x to_power n), 0 **] * [**x, 0 **]) by GROUP_1:def 7

 .= [**((x to_power n) * (x to_power 1)), 0 **] by POWER: 25

 .= [**(x to_power (n + 1)), 0 **] by A1, POWER: 27;

 hence P[(n + 1)];

 end;

 (( power F_Complex ) . ( [**x, 0 **], 0 )) = ( 1r + ( 0 * )) by COMPLFLD: 8, GROUP_1:def 7

 .= [**(x to_power 0 ), 0 **] by POWER: 24;

 then

 A3: P[ 0 ];

 thus for n be Nat holds P[n] from NAT_1:sch 2( A3, A2);

 end;