bhsp_5.miz



    begin

    reserve X for RealUnitarySpace;

    reserve x,y,y1,y2 for Point of X;

    reserve xd for set;

    reserve i,j,n for Nat;

    theorem :: BHSP_5:1

    

     Th1: for D be set, p1,p2 be FinSequence of D holds p1 is one-to-one & p2 is one-to-one & ( rng p1) = ( rng p2) implies ( dom p1) = ( dom p2) & ex P be Permutation of ( dom p1) st p2 = (p1 * P) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1)

    proof

      let D be set, p1,p2 be FinSequence of D;

      assume that

       A1: p1 is one-to-one and

       A2: p2 is one-to-one and

       A3: ( rng p1) = ( rng p2);

      set P = ((p1 " ) * p2);

      ( len p1) = ( card ( rng p2)) by A1, A3, FINSEQ_4: 62

      .= ( len p2) by A2, FINSEQ_4: 62;

      

      then

       A4: ( dom p1) = ( Seg ( len p2)) by FINSEQ_1:def 3

      .= ( dom p2) by FINSEQ_1:def 3;

       A5:

      now

        let xd be object;

        ( dom (p1 " )) = ( rng p1) by A1, FUNCT_1: 33;

        then xd in ( dom p2) implies (p2 . xd) in ( dom (p1 " )) by A3, FUNCT_1: 3;

        hence xd in ( dom P) iff xd in ( dom p2) by FUNCT_1: 11;

      end;

      then

       A6: ( dom P) = ( dom p2) by TARSKI: 2;

      

       A7: ( rng (p1 " )) = ( dom p1) by A1, FUNCT_1: 33;

      

       A8: ( rng P) c= ( dom p1) by A7, FUNCT_1: 14;

      

       A9: ( dom p1) c= ( rng P)

      proof

        let xd be object;

        assume xd in ( dom p1);

        then xd in ( rng (p1 " )) by A1, FUNCT_1: 33;

        then

        consider yd be object such that

         A10: yd in ( dom (p1 " )) and

         A11: xd = ((p1 " ) . yd) by FUNCT_1:def 3;

        yd in ( rng p2) by A1, A3, A10, FUNCT_1: 33;

        then

        consider z be object such that

         A12: z in ( dom p2) and

         A13: yd = (p2 . z) by FUNCT_1:def 3;

        xd = (P . z) by A11, A12, A13, FUNCT_1: 13;

        hence thesis by A6, A12, FUNCT_1:def 3;

      end;

      

       A14: ( dom P) = ( dom p1) by A4, A5, TARSKI: 2;

      

       A15: ( rng P) = ( dom p1) by A8, A9, XBOOLE_0:def 10;

      then P is Function of ( dom p1), ( dom p1) by A14, FUNCT_2: 1;

      then

       A16: P is Permutation of ( dom p1) by A1, A2, A15, FUNCT_2: 57;

      now

        let xd be object;

        xd in ( dom P) implies (P . xd) in ( dom p1) by A15, FUNCT_1: 3;

        hence xd in ( dom (p1 * P)) iff xd in ( dom p1) by A14, FUNCT_1: 11;

      end;

      then

       A17: ( dom p2) = ( dom (p1 * P)) by A4, TARSKI: 2;

      for xd be object st xd in ( dom p2) holds (p2 . xd) = ((p1 * P) . xd)

      proof

        let xd be object;

        assume

         A18: xd in ( dom p2);

        then

         A19: (p2 . xd) in ( rng p1) by A3, FUNCT_1: 3;

        ((p1 * P) . xd) = (p1 . (((p1 " ) * p2) . xd)) by A4, A14, A18, FUNCT_1: 13

        .= (p1 . ((p1 " ) . (p2 . xd))) by A18, FUNCT_1: 13

        .= (p2 . xd) by A1, A19, FUNCT_1: 35;

        hence thesis;

      end;

      hence thesis by A4, A14, A15, A16, A17, FUNCT_1: 2;

    end;

    definition

      let DX be non empty set;

      let f be BinOp of DX;

      let Y be finite Subset of DX;

      :: BHSP_5:def1

      func f ++ Y -> Element of DX means ex p be FinSequence of DX st p is one-to-one & ( rng p) = Y & it = (f "**" p);

      existence

      proof

        consider p be FinSequence such that

         A3: ( rng p) = Y and

         A4: p is one-to-one by FINSEQ_4: 58;

        reconsider q = p as FinSequence of DX by A3, FINSEQ_1:def 4;

        ex p be FinSequence of DX st p is one-to-one & ( rng p) = Y & (f "**" q) = (f "**" p) by A3, A4;

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be Element of DX such that

         A5: ex p1 be FinSequence of DX st p1 is one-to-one & ( rng p1) = Y & X1 = (f "**" p1) and

         A6: ex p2 be FinSequence of DX st p2 is one-to-one & ( rng p2) = Y & X2 = (f "**" p2);

        consider p1 be FinSequence of DX such that

         A7: p1 is one-to-one and

         A8: ( rng p1) = Y and

         A9: X1 = (f "**" p1) by A5;

        consider p2 be FinSequence of DX such that

         A10: p2 is one-to-one and

         A11: ( rng p2) = Y and

         A12: X2 = (f "**" p2) by A6;

        ex P be Permutation of ( dom p1) st p2 = (p1 * P) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1) by A7, A8, A10, A11, Th1;

        hence thesis by A1, A2, A9, A12, FINSOP_1: 7;

      end;

    end

    definition

      let X;

      let Y be finite Subset of X;

      :: BHSP_5:def2

      func setop_SUM (Y,X) -> set equals (the addF of X ++ Y) if Y <> {}

      otherwise ( 0. X);

      correctness ;

    end

    definition

      let X, x;

      let p be FinSequence;

      let i be Nat;

      :: BHSP_5:def3

      func PO (i,p,x) -> set equals (the scalar of X . [x, (p . i)]);

      correctness ;

    end

    definition

      let DK,DX be non empty set;

      let F be Function of DX, DK;

      let p be FinSequence of DX;

      :: BHSP_5:def4

      func Func_Seq (F,p) -> FinSequence of DK equals (F * p);

      correctness by FINSEQ_2: 32;

    end

    definition

      let DK,DX be non empty set;

      let f be BinOp of DK;

      let Y be finite Subset of DX;

      let F be Function of DX, DK;

      

       A3: ( dom F) = DX by FUNCT_2:def 1;

      :: BHSP_5:def5

      func setopfunc (Y,DX,DK,F,f) -> Element of DK means

      : Def5: ex p be FinSequence of DX st p is one-to-one & ( rng p) = Y & it = (f "**" ( Func_Seq (F,p)));

      existence

      proof

        consider p be FinSequence such that

         A4: ( rng p) = Y and

         A5: p is one-to-one by FINSEQ_4: 58;

        reconsider q = p as FinSequence of DX by A4, FINSEQ_1:def 4;

        ex p be FinSequence of DX st p is one-to-one & ( rng p) = Y & (f "**" ( Func_Seq (F,q))) = (f "**" ( Func_Seq (F,p))) by A4, A5;

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be Element of DK such that

         A6: ex p1 be FinSequence of DX st p1 is one-to-one & ( rng p1) = Y & X1 = (f "**" ( Func_Seq (F,p1))) and

         A7: ex p2 be FinSequence of DX st p2 is one-to-one & ( rng p2) = Y & X2 = (f "**" ( Func_Seq (F,p2)));

        consider p1 be FinSequence of DX such that

         A8: p1 is one-to-one and

         A9: ( rng p1) = Y and

         A10: X1 = (f "**" ( Func_Seq (F,p1))) by A6;

        consider p2 be FinSequence of DX such that

         A11: p2 is one-to-one and

         A12: ( rng p2) = Y and

         A13: X2 = (f "**" ( Func_Seq (F,p2))) by A7;

        

         A14: ( dom p1) = ( dom p2) by A8, A9, A11, A12, Th1;

        consider P be Permutation of ( dom p1) such that

         A15: p2 = (p1 * P) and ( dom P) = ( dom p1) and ( rng P) = ( dom p1) by A8, A9, A11, A12, Th1;

        now

          let xd be object;

          xd in ( dom p1) implies (p1 . xd) in ( rng p1) by FUNCT_1: 3;

          hence xd in ( dom ( Func_Seq (F,p1))) iff xd in ( dom p1) by A3, A9, FUNCT_1: 11;

        end;

        then

         A16: ( dom ( Func_Seq (F,p1))) = ( dom p1) by TARSKI: 2;

        now

          let xd be object;

          xd in ( dom p2) implies (p2 . xd) in ( rng p2) by FUNCT_1: 3;

          hence xd in ( dom ( Func_Seq (F,p2))) iff xd in ( dom p2) by A3, A12, FUNCT_1: 11;

        end;

        then

         A17: ( dom ( Func_Seq (F,p2))) = ( dom p2) by TARSKI: 2;

        

         A18: ( rng P) = ( dom ( Func_Seq (F,p1))) by A16, FUNCT_2:def 3;

        now

          let xd be object;

          xd in ( dom P) implies (P . xd) in ( dom ( Func_Seq (F,p1))) by A18, FUNCT_1: 3;

          then xd in ( dom (( Func_Seq (F,p1)) * P)) iff xd in ( dom P) by FUNCT_1: 11;

          hence xd in ( dom (( Func_Seq (F,p1)) * P)) iff xd in ( dom ( Func_Seq (F,p2))) by A14, A17, FUNCT_2: 52;

        end;

        then

         A19: ( dom ( Func_Seq (F,p2))) = ( dom (( Func_Seq (F,p1)) * P)) by TARSKI: 2;

        now

          let s be object;

          assume

           A20: s in ( dom ( Func_Seq (F,p2)));

          then

          reconsider i = s as Element of NAT ;

          i in ( dom P) by A14, A17, A20, FUNCT_2: 52;

          then

           A21: (P . i) in ( rng P) by FUNCT_1: 3;

          then (P . i) in ( dom ( Func_Seq (F,p2))) by A14, A17, FUNCT_2:def 3;

          then

          reconsider j = (P . i) as Element of NAT ;

          

           A22: j in ( dom p1) by A21, FUNCT_2:def 3;

          

           A23: s in ( dom P) by A14, A17, A20, FUNCT_2: 52;

          (( Func_Seq (F,p2)) . s) = (F . (p2 . i)) by A17, A20, FUNCT_1: 13

          .= (F . (p1 . (P . i))) by A15, A23, FUNCT_1: 13

          .= (( Func_Seq (F,p1)) . j) by A22, FUNCT_1: 13

          .= ((( Func_Seq (F,p1)) * P) . s) by A23, FUNCT_1: 13;

          hence (( Func_Seq (F,p2)) . s) = ((( Func_Seq (F,p1)) * P) . s);

        end;

        then ( Func_Seq (F,p2)) = (( Func_Seq (F,p1)) * P) by A19, FUNCT_1: 2;

        hence thesis by A1, A2, A10, A13, A16, FINSOP_1: 7;

      end;

    end

    definition

      let X, x;

      let Y be finite Subset of X;

      :: BHSP_5:def6

      func setop_xPre_PROD (x,Y,X) -> Real means ex p be FinSequence of the carrier of X st p is one-to-one & ( rng p) = Y & ex q be FinSequence of REAL st ( dom q) = ( dom p) & (for i st i in ( dom q) holds (q . i) = ( PO (i,p,x))) & it = ( addreal "**" q);

      existence

      proof

        consider p0 be FinSequence such that

         A1: ( rng p0) = Y and

         A2: p0 is one-to-one by FINSEQ_4: 58;

        reconsider p = p0 as FinSequence of the carrier of X by A1, FINSEQ_1:def 4;

        set ll = ( len p);

        deffunc F( Nat) = ( PO ($1,p,x));

        consider q0 be FinSequence such that

         A3: ( len q0) = ll & for i be Nat st i in ( dom q0) holds (q0 . i) = F(i) from FINSEQ_1:sch 2;

        

         A4: ( dom q0) = ( Seg ll) by A3, FINSEQ_1:def 3;

        

         A5: ( dom q0) = ( dom p) by A3, FINSEQ_3: 29;

        now

          let i be Nat;

          assume

           A6: i in ( dom q0);

          

          then

           A7: (q0 . i) = ( PO (i,p,x)) by A3

          .= (the scalar of X . [x, (p . i)]);

          reconsider y = (p . i) as Point of X by A5, A6, FINSEQ_2: 11;

          (the scalar of X . [x, (p . i)]) = (x .|. y) by BHSP_1:def 1;

          hence (q0 . i) in REAL by A7, XREAL_0:def 1;

        end;

        then

        reconsider q = q0 as FinSequence of REAL by FINSEQ_2: 12;

        take ( addreal "**" q), p;

        thus p is one-to-one & ( rng p) = Y by A1, A2;

        take q;

        thus thesis by A3, A4, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let X1,X2 be Real such that

         A8: ex p1 be FinSequence of the carrier of X st p1 is one-to-one & ( rng p1) = Y & ex q1 be FinSequence of REAL st ( dom q1) = ( dom p1) & (for i st i in ( dom q1) holds (q1 . i) = ( PO (i,p1,x))) & X1 = ( addreal "**" q1) and

         A9: ex p2 be FinSequence of the carrier of X st p2 is one-to-one & ( rng p2) = Y & ex q2 be FinSequence of REAL st ( dom q2) = ( dom p2) & (for i st i in ( dom q2) holds (q2 . i) = ( PO (i,p2,x))) & X2 = ( addreal "**" q2);

        consider p1 be FinSequence of the carrier of X such that

         A10: p1 is one-to-one and

         A11: ( rng p1) = Y and

         A12: ex q1 be FinSequence of REAL st ( dom q1) = ( dom p1) & (for i st i in ( dom q1) holds (q1 . i) = ( PO (i,p1,x))) & X1 = ( addreal "**" q1) by A8;

        consider p2 be FinSequence of the carrier of X such that

         A13: p2 is one-to-one and

         A14: ( rng p2) = Y and

         A15: ex q2 be FinSequence of REAL st ( dom q2) = ( dom p2) & (for i st i in ( dom q2) holds (q2 . i) = ( PO (i,p2,x))) & X2 = ( addreal "**" q2) by A9;

        consider q1 be FinSequence of REAL such that

         A16: ( dom q1) = ( dom p1) and

         A17: for i st i in ( dom q1) holds (q1 . i) = ( PO (i,p1,x)) and

         A18: X1 = ( addreal "**" q1) by A12;

        consider q2 be FinSequence of REAL such that

         A19: ( dom q2) = ( dom p2) and

         A20: for i st i in ( dom q2) holds (q2 . i) = ( PO (i,p2,x)) and

         A21: X2 = ( addreal "**" q2) by A15;

        

         A22: ( dom p1) = ( dom p2) by A10, A11, A13, A14, Th1;

        consider P be Permutation of ( dom p1) such that

         A23: p2 = (p1 * P) and ( dom P) = ( dom p1) and ( rng P) = ( dom p1) by A10, A11, A13, A14, Th1;

        

         A24: ( rng P) = ( dom q1) by A16, FUNCT_2:def 3;

        

         A25: ( dom P) = ( dom q2) by A19, A22, FUNCT_2: 52;

        

         A26: ( rng P) = ( dom q2) by A19, A22, FUNCT_2:def 3;

        

         A27: ( dom p1) = ( dom q2) by A10, A11, A13, A14, A19, Th1;

        now

          let xd be object;

          xd in ( dom P) implies (P . xd) in ( dom q1) by A24, FUNCT_1: 3;

          hence xd in ( dom (q1 * P)) iff xd in ( dom q2) by A25, FUNCT_1: 11;

        end;

        then

         A28: ( dom q2) = ( dom (q1 * P)) by TARSKI: 2;

        now

          let s be object;

          assume

           A29: s in ( dom q2);

          then

          reconsider i = s as Element of NAT ;

          (P . i) in ( dom q2) by A25, A26, A29, FUNCT_1: 3;

          then

          reconsider j = (P . i) as Element of NAT ;

          

           A30: s in ( dom P) by A19, A22, A29, FUNCT_2: 52;

          (q2 . s) = ( PO (i,p2,x)) by A20, A29

          .= ( PO (j,p1,x)) by A23, A30, FUNCT_1: 13

          .= (q1 . (P . i)) by A16, A17, A25, A26, A27, A29, FUNCT_1: 3

          .= ((q1 * P) . s) by A30, FUNCT_1: 13;

          hence (q2 . s) = ((q1 * P) . s);

        end;

        then q2 = (q1 * P) by A28, FUNCT_1: 2;

        hence thesis by A16, A18, A21, FINSOP_1: 7;

      end;

    end

    definition

      let X, x;

      let Y be finite Subset of X;

      :: BHSP_5:def7

      func setop_xPROD (x,Y,X) -> Real equals ( setop_xPre_PROD (x,Y,X)) if Y <> {}

      otherwise 0 ;

      correctness ;

    end

    begin

    definition

      let X;

      :: BHSP_5:def8

      mode OrthogonalFamily of X -> Subset of X means

      : Def8: for x, y st x in it & y in it & x <> y holds (x .|. y) = 0 ;

      existence

      proof

        take {} ;

        thus thesis by SUBSET_1: 1;

      end;

    end

    theorem :: BHSP_5:2

    

     Th2: {} is OrthogonalFamily of X

    proof

      

       A1: {} is Subset of X by SUBSET_1: 1;

      x in {} & y in {} & x <> y implies (x .|. y) = 0 ;

      hence thesis by A1, Def8;

    end;

    registration

      let X;

      cluster finite for OrthogonalFamily of X;

      existence

      proof

        take {} ;

        thus thesis by Th2;

      end;

    end

    definition

      let X;

      :: BHSP_5:def9

      mode OrthonormalFamily of X -> Subset of X means

      : Def9: it is OrthogonalFamily of X & for x st x in it holds (x .|. x) = 1;

      existence

      proof

        take {} ;

        thus thesis by Th2;

      end;

    end

    theorem :: BHSP_5:3

    

     Th3: {} is OrthonormalFamily of X

    proof

      

       A1: {} is OrthogonalFamily of X by Th2;

      x in {} implies (x .|. x) = 1;

      hence thesis by A1, Def9;

    end;

    registration

      let X;

      cluster finite for OrthonormalFamily of X;

      existence

      proof

        take {} ;

        thus thesis by Th3;

      end;

    end

    theorem :: BHSP_5:4

    x = ( 0. X) iff for y holds (x .|. y) = 0

    proof

      now

        assume for y holds (x .|. y) = 0 ;

        then (x .|. x) = 0 ;

        hence x = ( 0. X) by BHSP_1:def 2;

      end;

      hence thesis by BHSP_1: 14;

    end;

    begin

    theorem :: BHSP_5:5

    (( ||.(x + y).|| ^2 ) + ( ||.(x - y).|| ^2 )) = ((2 * ( ||.x.|| ^2 )) + (2 * ( ||.y.|| ^2 )))

    proof

      

       A1: ((x + y) .|. (x + y)) >= 0 by BHSP_1:def 2;

      

       A2: ((x - y) .|. (x - y)) >= 0 by BHSP_1:def 2;

      

       A3: (x .|. x) >= 0 by BHSP_1:def 2;

      

       A4: (y .|. y) >= 0 by BHSP_1:def 2;

      (( ||.(x + y).|| ^2 ) + ( ||.(x - y).|| ^2 )) = ((( sqrt ((x + y) .|. (x + y))) ^2 ) + ( ||.(x - y).|| ^2 )) by BHSP_1:def 4

      .= (((x + y) .|. (x + y)) + ( ||.(x - y).|| ^2 )) by A1, SQUARE_1:def 2

      .= (((x + y) .|. (x + y)) + (( sqrt ((x - y) .|. (x - y))) ^2 )) by BHSP_1:def 4

      .= (((x + y) .|. (x + y)) + ((x - y) .|. (x - y))) by A2, SQUARE_1:def 2

      .= ((((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + ((x - y) .|. (x - y))) by BHSP_1: 16

      .= ((((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + (((x .|. x) - (2 * (x .|. y))) + (y .|. y))) by BHSP_1: 18

      .= ((2 * (x .|. x)) + (2 * (y .|. y)))

      .= ((2 * (( sqrt (x .|. x)) ^2 )) + (2 * (y .|. y))) by A3, SQUARE_1:def 2

      .= ((2 * (( sqrt (x .|. x)) ^2 )) + (2 * (( sqrt (y .|. y)) ^2 ))) by A4, SQUARE_1:def 2

      .= ((2 * ( ||.x.|| ^2 )) + (2 * (( sqrt (y .|. y)) ^2 ))) by BHSP_1:def 4

      .= ((2 * ( ||.x.|| ^2 )) + (2 * ( ||.y.|| ^2 ))) by BHSP_1:def 4;

      hence thesis;

    end;

    theorem :: BHSP_5:6

    (x,y) are_orthogonal implies ( ||.(x + y).|| ^2 ) = (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))

    proof

      assume (x,y) are_orthogonal ;

      then

       A1: (x .|. y) = 0 by BHSP_1:def 3;

      

       A2: ((x + y) .|. (x + y)) >= 0 by BHSP_1:def 2;

      

       A3: (x .|. x) >= 0 by BHSP_1:def 2;

      

       A4: (y .|. y) >= 0 by BHSP_1:def 2;

      ( ||.(x + y).|| ^2 ) = (( sqrt ((x + y) .|. (x + y))) ^2 ) by BHSP_1:def 4

      .= ((x + y) .|. (x + y)) by A2, SQUARE_1:def 2

      .= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) by BHSP_1: 16

      .= ((( sqrt (x .|. x)) ^2 ) + (y .|. y)) by A1, A3, SQUARE_1:def 2

      .= ((( sqrt (x .|. x)) ^2 ) + (( sqrt (y .|. y)) ^2 )) by A4, SQUARE_1:def 2

      .= (( ||.x.|| ^2 ) + (( sqrt (y .|. y)) ^2 )) by BHSP_1:def 4

      .= (( ||.x.|| ^2 ) + ( ||.y.|| ^2 )) by BHSP_1:def 4;

      hence thesis;

    end;

    theorem :: BHSP_5:7

    

     Th7: for p be FinSequence of the carrier of X st (( len p) >= 1 & for i, j st i in ( dom p) & j in ( dom p) & i <> j holds (the scalar of X . [(p . i), (p . j)]) = 0 ) holds for q be FinSequence of REAL st ( dom p) = ( dom q) & (for i st i in ( dom q) holds (q . i) = (the scalar of X . [(p . i), (p . i)])) holds ((the addF of X "**" p) .|. (the addF of X "**" p)) = ( addreal "**" q)

    proof

      let p be FinSequence of the carrier of X;

      assume that

       A1: ( len p) >= 1 and

       A2: for i, j st i in ( dom p) & j in ( dom p) & i <> j holds (the scalar of X . [(p . i), (p . j)]) = 0 ;

      

       A3: 1 in ( dom p) by A1, FINSEQ_3: 25;

      let q be FinSequence of REAL such that

       A4: ( dom p) = ( dom q) and

       A5: for i st i in ( dom q) holds (q . i) = (the scalar of X . [(p . i), (p . i)]);

      consider f be sequence of the carrier of X such that

       A6: (f . 1) = (p . 1) and

       A7: for n be Nat st 0 <> n & n < ( len p) holds (f . (n + 1)) = (the addF of X . ((f . n),(p . (n + 1)))) and

       A8: (the addF of X "**" p) = (f . ( len p)) by A1, FINSOP_1: 1;

      

       A9: ((the addF of X "**" p) .|. (the addF of X "**" p)) = (the scalar of X . [(f . ( len p)), (f . ( len p))]) by A8, BHSP_1:def 1;

      

       A10: ( Seg ( len q)) = ( dom p) by A4, FINSEQ_1:def 3

      .= ( Seg ( len p)) by FINSEQ_1:def 3;

      then

       A11: ( len q) = ( len p) by FINSEQ_1: 6;

      ( len q) >= 1 by A1, A10, FINSEQ_1: 6;

      then

      consider g be sequence of REAL such that

       A12: (g . 1) = (q . 1) and

       A13: for n be Nat st 0 <> n & n < ( len q) holds (g . (n + 1)) = ( addreal . ((g . n),(q . (n + 1)))) and

       A14: ( addreal "**" q) = (g . ( len q)) by FINSOP_1: 1;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len q) implies (g . $1) = (the scalar of X . [(f . $1), (f . $1)]);

      

       A15: P[ 0 ];

      now

        let n;

        assume that

         A16: 1 <= n & n <= ( len q) implies (g . n) = (the scalar of X . [(f . n), (f . n)]);

        now

          assume that

           A17: 1 <= (n + 1) and

           A18: (n + 1) <= ( len q);

          

           A19: n <= (n + 1) by NAT_1: 11;

          per cases ;

            suppose

             A20: n = 0 ;

            1 in ( Seg ( len p)) by A1, FINSEQ_1: 1;

            then 1 in ( dom q) by A4, FINSEQ_1:def 3;

            hence (g . (n + 1)) = (the scalar of X . [(f . (n + 1)), (f . (n + 1))]) by A5, A6, A12, A20;

          end;

            suppose

             A21: n <> 0 ;

            then 0 < n;

            then

             A22: ( 0 + 1) <= n by INT_1: 7;

            

             A23: n <= ( len p) by A11, A18, A19, XXREAL_0: 2;

            

             A24: ((n + 1) - 1) < (( len q) - 0 ) by A18, XREAL_1: 15;

            then

             A25: n < ( len p) by A10, FINSEQ_1: 6;

            

             A26: (n + 1) in ( Seg ( len q)) by A17, A18, FINSEQ_1: 1;

            then

             A27: (n + 1) in ( dom q) by FINSEQ_1:def 3;

            

             A28: (n + 1) in ( dom p) by A4, A26, FINSEQ_1:def 3;

            

             A29: n in NAT by ORDINAL1:def 12;

            

             A30: ( dom f) = NAT by FUNCT_2:def 1;

            then

             A31: (f . n) in ( rng f) by FUNCT_1: 3, A29;

            ( rng f) c= the carrier of X by RELAT_1:def 19;

            then

            reconsider z = (f . n) as Element of X by A31;

            

             A32: (p . (n + 1)) in ( rng p) by A28, FUNCT_1: 3;

            ( rng p) c= the carrier of X by RELAT_1:def 19;

            then

            reconsider y = (p . (n + 1)) as Element of X by A32;

            for i st 1 <= i & i <= n holds (the scalar of X . [(f . i), y]) = 0

            proof

              let i;

              defpred P[ Nat] means 1 <= $1 & $1 <= n implies (the scalar of X . [(f . $1), y]) = 0 ;

              

               A33: P[ 0 ];

              

               A34: for i st P[i] holds P[(i + 1)]

              proof

                let i;

                assume

                 A35: P[i];

                

                 A36: 1 <> (n + 1) by A21;

                assume that

                 A37: 1 <= (i + 1) and

                 A38: (i + 1) <= n;

                (i + 1) <= ( len p) by A23, A38, XXREAL_0: 2;

                then

                 A39: (i + 1) in ( dom p) by A37, FINSEQ_3: 25;

                

                 A40: i in NAT by ORDINAL1:def 12;

                per cases ;

                  suppose i = 0 ;

                  hence thesis by A2, A3, A6, A28, A36;

                end;

                  suppose

                   A41: i <> 0 ;

                  

                   A42: (f . i) in ( rng f) by A30, FUNCT_1: 3, A40;

                  ( rng f) c= the carrier of X by RELAT_1:def 19;

                  then

                  reconsider s = (f . i) as Element of X by A42;

                  

                   A43: (i + 1) <= ( len p) by A23, A38, XXREAL_0: 2;

                  then (i + 1) in ( dom p) by A37, FINSEQ_3: 25;

                  then

                   A44: (p . (i + 1)) in ( rng p) by FUNCT_1: 3;

                  ( rng p) c= the carrier of X by RELAT_1:def 19;

                  then

                  reconsider t = (p . (i + 1)) as Element of X by A44;

                  

                   A45: ((i + 1) - 1) < (( len p) - 0 ) by A43, XREAL_1: 15;

                   0 < i by A41;

                  then

                   A46: ( 0 + 1) <= i by INT_1: 7;

                  i < (i + 1) by XREAL_1: 29;

                  then

                   A47: (s .|. y) = 0 by A35, A38, A46, BHSP_1:def 1, XXREAL_0: 2;

                  

                   A48: ((i + 1) + 0 ) < (n + 1) by A38, XREAL_1: 8;

                  (the scalar of X . [(f . (i + 1)), y]) = (the scalar of X . [(s + t), y]) by A7, A41, A45

                  .= ((s + t) .|. y) by BHSP_1:def 1

                  .= ( 0 + (t .|. y)) by A47, BHSP_1: 2

                  .= (the scalar of X . [t, y]) by BHSP_1:def 1

                  .= 0 by A2, A28, A39, A48;

                  hence thesis;

                end;

              end;

              for i holds P[i] from NAT_1:sch 2( A33, A34);

              hence thesis;

            end;

            

            then

             A49: 0 = (the scalar of X . [z, y]) by A22

            .= (z .|. y) by BHSP_1:def 1;

            

            thus (g . (n + 1)) = ( addreal . ((the scalar of X . [(f . n), (f . n)]),(q . (n + 1)))) by A13, A16, A22, A24

            .= ( addreal . ((the scalar of X . [(f . n), (f . n)]),(the scalar of X . [(p . (n + 1)), (p . (n + 1))]))) by A5, A27

            .= ( addreal . ((the scalar of X . [(f . n), (f . n)]),(y .|. y))) by BHSP_1:def 1

            .= ( addreal . ((z .|. z),(y .|. y))) by BHSP_1:def 1

            .= ((((z .|. z) + (z .|. y)) + (y .|. z)) + (y .|. y)) by A49, BINOP_2:def 9

            .= (((z .|. (z + y)) + (y .|. z)) + (y .|. y)) by BHSP_1: 2

            .= ((z .|. (z + y)) + ((y .|. z) + (y .|. y)))

            .= ((z .|. (z + y)) + (y .|. (z + y))) by BHSP_1: 2

            .= ((z + y) .|. (z + y)) by BHSP_1: 2

            .= (the scalar of X . [(the addF of X . ((f . n),(p . (n + 1)))), (z + y)]) by BHSP_1:def 1

            .= (the scalar of X . [(the addF of X . ((f . n),(p . (n + 1)))), (f . (n + 1))]) by A7, A21, A25

            .= (the scalar of X . [(f . (n + 1)), (f . (n + 1))]) by A7, A21, A25;

          end;

        end;

        hence 1 <= (n + 1) & (n + 1) <= ( len q) implies (g . (n + 1)) = (the scalar of X . [(f . (n + 1)), (f . (n + 1))]);

      end;

      then

       A50: P[n] implies P[(n + 1)];

      for n holds P[n] from NAT_1:sch 2( A15, A50);

      hence thesis by A1, A9, A11, A14;

    end;

    theorem :: BHSP_5:8

    

     Th8: for p be FinSequence of the carrier of X st ( len p) >= 1 holds for q be FinSequence of REAL st ( dom p) = ( dom q) & (for i st i in ( dom q) holds (q . i) = (the scalar of X . [x, (p . i)])) holds (x .|. (the addF of X "**" p)) = ( addreal "**" q)

    proof

      let p be FinSequence of the carrier of X such that

       A1: ( len p) >= 1;

      let q be FinSequence of REAL such that

       A2: ( dom p) = ( dom q) and

       A3: for i st i in ( dom q) holds (q . i) = (the scalar of X . [x, (p . i)]);

      consider f be sequence of the carrier of X such that

       A4: (f . 1) = (p . 1) and

       A5: for n be Nat st 0 <> n & n < ( len p) holds (f . (n + 1)) = (the addF of X . ((f . n),(p . (n + 1)))) and

       A6: (the addF of X "**" p) = (f . ( len p)) by A1, FINSOP_1: 1;

      

       A7: ( Seg ( len q)) = ( dom p) by A2, FINSEQ_1:def 3

      .= ( Seg ( len p)) by FINSEQ_1:def 3;

      then

       A8: ( len q) = ( len p) by FINSEQ_1: 6;

      ( len q) >= 1 by A1, A7, FINSEQ_1: 6;

      then

      consider g be sequence of REAL such that

       A9: (g . 1) = (q . 1) and

       A10: for n be Nat st 0 <> n & n < ( len q) holds (g . (n + 1)) = ( addreal . ((g . n),(q . (n + 1)))) and

       A11: ( addreal "**" q) = (g . ( len q)) by FINSOP_1: 1;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len q) implies (g . $1) = (the scalar of X . [x, (f . $1)]);

      

       A12: P[ 0 ];

      now

        let n;

        assume

         A13: P[n];

        now

          assume that

           A14: 1 <= (n + 1) and

           A15: (n + 1) <= ( len q);

          per cases ;

            suppose

             A16: n = 0 ;

            1 in ( Seg ( len p)) by A1, FINSEQ_1: 1;

            then 1 in ( dom q) by A2, FINSEQ_1:def 3;

            hence (g . (n + 1)) = (the scalar of X . [x, (f . (n + 1))]) by A3, A4, A9, A16;

          end;

            suppose

             A17: n <> 0 ;

            then 0 < n;

            then

             A18: ( 0 + 1) <= n by INT_1: 7;

            

             A19: ((n + 1) - 1) < (( len q) - 0 ) by A15, XREAL_1: 15;

            

             A20: (n + 1) in ( Seg ( len q)) by A14, A15, FINSEQ_1: 1;

            then

             A21: (n + 1) in ( dom q) by FINSEQ_1:def 3;

            

             A22: (n + 1) in ( dom p) by A2, A20, FINSEQ_1:def 3;

            

             A23: n in NAT by ORDINAL1:def 12;

            ( dom f) = NAT by FUNCT_2:def 1;

            then

             A24: (f . n) in ( rng f) by FUNCT_1: 3, A23;

            ( rng f) c= the carrier of X by RELAT_1:def 19;

            then

            reconsider z = (f . n) as Element of X by A24;

            

             A25: (p . (n + 1)) in ( rng p) by A22, FUNCT_1: 3;

            ( rng p) c= the carrier of X by RELAT_1:def 19;

            then

            reconsider y = (p . (n + 1)) as Element of X by A25;

            

            thus (g . (n + 1)) = ( addreal . ((the scalar of X . [x, (f . n)]),(q . (n + 1)))) by A10, A13, A18, A19

            .= ( addreal . ((the scalar of X . [x, (f . n)]),(the scalar of X . [x, (p . (n + 1))]))) by A3, A21

            .= ( addreal . ((the scalar of X . [x, (f . n)]),(x .|. y))) by BHSP_1:def 1

            .= ( addreal . ((x .|. z),(x .|. y))) by BHSP_1:def 1

            .= ((x .|. z) + (x .|. y)) by BINOP_2:def 9

            .= (x .|. (z + y)) by BHSP_1: 2

            .= (the scalar of X . [x, (the addF of X . ((f . n),(p . (n + 1))))]) by BHSP_1:def 1

            .= (the scalar of X . [x, (f . (n + 1))]) by A5, A8, A17, A19;

          end;

        end;

        hence 1 <= (n + 1) & (n + 1) <= ( len q) implies (g . (n + 1)) = (the scalar of X . [x, (f . (n + 1))]);

      end;

      then

       A26: P[n] implies P[(n + 1)];

      

       A27: for n holds P[n] from NAT_1:sch 2( A12, A26);

      1 <= ( len q) by A1, A7, FINSEQ_1: 6;

      

      then (g . ( len q)) = (the scalar of X . [x, (f . ( len q))]) by A27

      .= (the scalar of X . [x, (f . ( len p))]) by A7, FINSEQ_1: 6;

      hence thesis by A6, A11, BHSP_1:def 1;

    end;

    theorem :: BHSP_5:9

    

     Th9: for S be finite non empty Subset of X holds for F be Function of the carrier of X, the carrier of X st S c= ( dom F) & (for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X . [(F . y1), (F . y2)]) = 0 ) holds for H be Function of the carrier of X, REAL st S c= ( dom H) & (for y st y in S holds (H . y) = (the scalar of X . [(F . y), (F . y)])) holds for p be FinSequence of the carrier of X st p is one-to-one & ( rng p) = S holds (the scalar of X . [(the addF of X "**" ( Func_Seq (F,p))), (the addF of X "**" ( Func_Seq (F,p)))]) = ( addreal "**" ( Func_Seq (H,p)))

    proof

      let S be finite non empty Subset of X;

      let F be Function of the carrier of X, the carrier of X such that

       A1: S c= ( dom F) and

       A2: for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X . [(F . y1), (F . y2)]) = 0 ;

      let H be Function of the carrier of X, REAL such that

       A3: S c= ( dom H) and

       A4: for y st y in S holds (H . y) = (the scalar of X . [(F . y), (F . y)]);

      let p be FinSequence of the carrier of X such that

       A5: p is one-to-one and

       A6: ( rng p) = S;

      set fp = ( Func_Seq (F,p));

      set hp = ( Func_Seq (H,p));

      now

        let z be object;

        z in ( dom p) implies (p . z) in ( rng p) by FUNCT_1: 3;

        hence z in ( dom fp) iff z in ( dom p) by A1, A6, FUNCT_1: 11;

      end;

      then

       A7: ( dom fp) = ( dom p) by TARSKI: 2;

      

      then

       A8: ( Seg ( len p)) = ( dom fp) by FINSEQ_1:def 3

      .= ( Seg ( len fp)) by FINSEQ_1:def 3;

      

       A9: ( len p) = ( card S) by A5, A6, FINSEQ_4: 62;

       0 < ( card S);

      then ( 0 + 1) <= ( card S) by INT_1: 7;

      then

       A10: 1 <= ( len fp) by A8, A9, FINSEQ_1: 6;

      

       A11: for i, j st i in ( dom fp) & j in ( dom fp) & i <> j holds (the scalar of X . [(fp . i), (fp . j)]) = 0

      proof

        let i, j;

        assume that

         A12: i in ( dom fp) and

         A13: j in ( dom fp) and

         A14: i <> j;

        

         A15: (p . i) in S by A6, A7, A12, FUNCT_1: 3;

        

         A16: (p . j) in S by A6, A7, A13, FUNCT_1: 3;

        

         A17: (fp . i) = (F . (p . i)) by A12, FUNCT_1: 12;

        

         A18: (fp . j) = (F . (p . j)) by A13, FUNCT_1: 12;

        (p . i) <> (p . j) by A5, A7, A12, A13, A14, FUNCT_1:def 4;

        hence thesis by A2, A15, A16, A17, A18;

      end;

      now

        let z be object;

        z in ( dom p) implies (p . z) in ( rng p) by FUNCT_1: 3;

        hence z in ( dom hp) iff z in ( dom p) by A3, A6, FUNCT_1: 11;

      end;

      then

       A19: ( dom hp) = ( dom p) by TARSKI: 2;

      

       A20: for i st i in ( dom hp) holds (hp . i) = (the scalar of X . [(fp . i), (fp . i)])

      proof

        let i such that

         A21: i in ( dom hp);

        

         A22: (p . i) in S by A6, A19, A21, FUNCT_1: 3;

        (hp . i) = (H . (p . i)) by A19, A21, FUNCT_1: 13

        .= (the scalar of X . [(F . (p . i)), (F . (p . i))]) by A4, A22

        .= (the scalar of X . [((F * p) . i), (F . (p . i))]) by A19, A21, FUNCT_1: 13

        .= (the scalar of X . [(fp . i), (fp . i)]) by A19, A21, FUNCT_1: 13;

        hence thesis;

      end;

      (the scalar of X . [(the addF of X "**" ( Func_Seq (F,p))), (the addF of X "**" ( Func_Seq (F,p)))]) = ((the addF of X "**" fp) .|. (the addF of X "**" fp)) by BHSP_1:def 1

      .= ( addreal "**" ( Func_Seq (H,p))) by A7, A10, A11, A19, A20, Th7;

      hence thesis;

    end;

    theorem :: BHSP_5:10

    

     Th10: for S be finite non empty Subset of X holds for F be Function of the carrier of X, the carrier of X st S c= ( dom F) holds for H be Function of the carrier of X, REAL st S c= ( dom H) & (for y st y in S holds (H . y) = (the scalar of X . [x, (F . y)])) holds for p be FinSequence of the carrier of X st p is one-to-one & ( rng p) = S holds (the scalar of X . [x, (the addF of X "**" ( Func_Seq (F,p)))]) = ( addreal "**" ( Func_Seq (H,p)))

    proof

      let S be finite non empty Subset of X;

      let F be Function of the carrier of X, the carrier of X such that

       A1: S c= ( dom F);

      let H be Function of the carrier of X, REAL such that

       A2: S c= ( dom H) and

       A3: for y st y in S holds (H . y) = (the scalar of X . [x, (F . y)]);

      let p be FinSequence of the carrier of X such that

       A4: p is one-to-one and

       A5: ( rng p) = S;

      set p1 = ( Func_Seq (F,p));

      set q1 = ( Func_Seq (H,p));

      now

        let xd be object;

        xd in ( dom p) implies (p . xd) in ( rng p) by FUNCT_1: 3;

        hence xd in ( dom ( Func_Seq (F,p))) iff xd in ( dom p) by A1, A5, FUNCT_1: 11;

      end;

      then

       A6: ( dom ( Func_Seq (F,p))) = ( dom p) by TARSKI: 2;

      now

        let xd be object;

        xd in ( dom p) implies (p . xd) in ( rng p) by FUNCT_1: 3;

        hence xd in ( dom ( Func_Seq (H,p))) iff xd in ( dom p) by A2, A5, FUNCT_1: 11;

      end;

      then

       A7: ( dom ( Func_Seq (H,p))) = ( dom p) by TARSKI: 2;

      

       A8: for i st i in ( dom p1) holds (q1 . i) = (the scalar of X . [x, (p1 . i)])

      proof

        let i such that

         A9: i in ( dom p1);

        

         A10: (p . i) in S by A5, A6, A9, FUNCT_1: 3;

        (q1 . i) = (H . (p . i)) by A6, A9, FUNCT_1: 13

        .= (the scalar of X . [x, (F . (p . i))]) by A3, A10

        .= (the scalar of X . [x, (p1 . i)]) by A6, A9, FUNCT_1: 13;

        hence thesis;

      end;

      

       A11: ( Seg ( len p)) = ( dom ( Func_Seq (F,p))) by A6, FINSEQ_1:def 3

      .= ( Seg ( len ( Func_Seq (F,p)))) by FINSEQ_1:def 3;

      

       A12: ( len p) = ( card S) by A4, A5, FINSEQ_4: 62;

       0 < ( card S);

      then ( 0 + 1) <= ( card S) by INT_1: 7;

      then ( len ( Func_Seq (F,p))) >= 1 by A11, A12, FINSEQ_1: 6;

      then (x .|. (the addF of X "**" p1)) = ( addreal "**" q1) by A6, A7, A8, Th8;

      hence thesis by BHSP_1:def 1;

    end;

    theorem :: BHSP_5:11

    

     Th11: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for x holds for S be finite OrthonormalFamily of X st S is non empty holds for H be Function of the carrier of X, REAL st S c= ( dom H) & (for y st y in S holds (H . y) = ((x .|. y) ^2 )) holds for F be Function of the carrier of X, the carrier of X st S c= ( dom F) & (for y st y in S holds (F . y) = ((x .|. y) * y)) holds (x .|. ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X))) = ( setopfunc (S,the carrier of X, REAL ,H, addreal ))

    proof

      let X such that

       A1: the addF of X is commutative associative and

       A2: the addF of X is having_a_unity;

      let x;

      let S be finite OrthonormalFamily of X such that

       A3: S is non empty;

      let H be Function of the carrier of X, REAL such that

       A4: S c= ( dom H) and

       A5: for y st y in S holds (H . y) = ((x .|. y) ^2 );

      let F be Function of the carrier of X, the carrier of X such that

       A6: S c= ( dom F) and

       A7: for y st y in S holds (F . y) = ((x .|. y) * y);

      consider p be FinSequence of the carrier of X such that

       A8: p is one-to-one and

       A9: ( rng p) = S and

       A10: ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X)) = (the addF of X "**" ( Func_Seq (F,p))) by A1, A2, Def5;

      

       A11: for y st y in S holds (H . y) = (the scalar of X . [x, (F . y)])

      proof

        let y such that

         A12: y in S;

        set a = (x .|. y);

        (H . y) = ((x .|. y) ^2 ) by A5, A12

        .= (x .|. (a * y)) by BHSP_1: 3

        .= (the scalar of X . [x, (a * y)]) by BHSP_1:def 1

        .= (the scalar of X . [x, (F . y)]) by A7, A12;

        hence thesis;

      end;

      

       A13: ( setopfunc (S,the carrier of X, REAL ,H, addreal )) = ( addreal "**" ( Func_Seq (H,p))) by A8, A9, Def5;

      (x .|. ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X))) = (the scalar of X . [x, (the addF of X "**" ( Func_Seq (F,p)))]) by A10, BHSP_1:def 1;

      hence thesis by A3, A4, A6, A8, A9, A11, A13, Th10;

    end;

    theorem :: BHSP_5:12

    

     Th12: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for x holds for S be finite OrthonormalFamily of X st S is non empty holds for F be Function of the carrier of X, the carrier of X st S c= ( dom F) & (for y st y in S holds (F . y) = ((x .|. y) * y)) holds for H be Function of the carrier of X, REAL st S c= ( dom H) & (for y st y in S holds (H . y) = ((x .|. y) ^2 )) holds (( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X)) .|. ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X))) = ( setopfunc (S,the carrier of X, REAL ,H, addreal ))

    proof

      let X such that

       A1: the addF of X is commutative associative and

       A2: the addF of X is having_a_unity;

      let x;

      let S be finite OrthonormalFamily of X such that

       A3: S is non empty;

      let F be Function of the carrier of X, the carrier of X such that

       A4: S c= ( dom F) and

       A5: for y st y in S holds (F . y) = ((x .|. y) * y);

      let H be Function of the carrier of X, REAL such that

       A6: S c= ( dom H) and

       A7: for y st y in S holds (H . y) = ((x .|. y) ^2 );

      consider p be FinSequence of the carrier of X such that

       A8: p is one-to-one and

       A9: ( rng p) = S and

       A10: ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X)) = (the addF of X "**" ( Func_Seq (F,p))) by A1, A2, Def5;

      

       A11: for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X . [(F . y1), (F . y2)]) = 0

      proof

        let y1, y2;

        assume that

         A12: y1 in S and

         A13: y2 in S and

         A14: y1 <> y2;

        set z1 = (x .|. y1);

        set z2 = (x .|. y2);

        S is OrthogonalFamily of X by Def9;

        then

         A15: (y1 .|. y2) = 0 by A12, A13, A14, Def8;

        (the scalar of X . [(F . y1), (F . y2)]) = (the scalar of X . [((x .|. y1) * y1), (F . y2)]) by A5, A12

        .= (the scalar of X . [((x .|. y1) * y1), ((x .|. y2) * y2)]) by A5, A13

        .= ((z1 * y1) .|. (z2 * y2)) by BHSP_1:def 1

        .= (z2 * (y2 .|. (z1 * y1))) by BHSP_1: 3

        .= (z2 * (z1 * (y2 .|. y1))) by BHSP_1: 3

        .= 0 by A15;

        hence thesis;

      end;

      

       A16: for y st y in S holds (H . y) = (the scalar of X . [(F . y), (F . y)])

      proof

        let y;

        assume

         A17: y in S;

        then

         A18: (F . y) = ((x .|. y) * y) by A5;

        (H . y) = ((x .|. y) ^2 ) by A7, A17

        .= (((x .|. y) * (x .|. y)) * 1)

        .= (((x .|. y) * (x .|. y)) * (y .|. y)) by A17, Def9

        .= ((x .|. y) * ((x .|. y) * (y .|. y)))

        .= ((x .|. y) * (((x .|. y) * y) .|. y)) by BHSP_1: 3

        .= (((x .|. y) * y) .|. ((x .|. y) * y)) by BHSP_1: 3

        .= (the scalar of X . [(F . y), (F . y)]) by A18, BHSP_1:def 1;

        hence thesis;

      end;

      (( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X)) .|. ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X))) = (the scalar of X . [(the addF of X "**" ( Func_Seq (F,p))), (the addF of X "**" ( Func_Seq (F,p)))]) by A10, BHSP_1:def 1

      .= ( addreal "**" ( Func_Seq (H,p))) by A3, A4, A6, A8, A9, A11, A16, Th9

      .= ( setopfunc (S,the carrier of X, REAL ,H, addreal )) by A8, A9, Def5;

      hence thesis;

    end;

    theorem :: BHSP_5:13

    for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for x holds for S be finite OrthonormalFamily of X st S is non empty holds for H be Function of the carrier of X, REAL st S c= ( dom H) & (for y st y in S holds (H . y) = ((x .|. y) ^2 )) holds ( setopfunc (S,the carrier of X, REAL ,H, addreal )) <= ( ||.x.|| ^2 )

    proof

      let X such that

       A1: the addF of X is commutative associative and

       A2: the addF of X is having_a_unity;

      let x;

      let S be finite OrthonormalFamily of X such that

       A3: S is non empty;

      let H be Function of the carrier of X, REAL such that

       A4: S c= ( dom H) and

       A5: for y st y in S holds (H . y) = ((x .|. y) ^2 );

      now

        deffunc F( object) = (the Mult of X . [(the scalar of X . [x, $1]), $1]);

        

         A6: for y be object st y in the carrier of X holds F(y) in the carrier of X

        proof

          let y be object such that

           A7: y in the carrier of X;

          reconsider y1 = y as Point of X by A7;

          set x1 = x;

          (the scalar of X . [x, y]) = (x1 .|. y1) by BHSP_1:def 1;

          then

          reconsider a = (the scalar of X . [x, y]) as Real;

          reconsider y2 = y as VECTOR of X by A7;

          (the Mult of X . ((the scalar of X . [x, y]),y)) = (a * y2);

          hence thesis;

        end;

        ex F0 be Function of the carrier of X, the carrier of X st for y be object st y in the carrier of X holds (F0 . y) = F(y) from FUNCT_2:sch 2( A6);

        then

        consider F0 be Function of the carrier of X, the carrier of X such that

         A8: for y be object st y in the carrier of X holds (F0 . y) = (the Mult of X . [(the scalar of X . [x, y]), y]);

        

         A9: ( dom F0) = the carrier of X by FUNCT_2:def 1;

        now

          let y such that y in S;

          

          thus (F0 . y) = (the Mult of X . [(the scalar of X . [x, y]), y]) by A8

          .= ((x .|. y) * y) by BHSP_1:def 1;

        end;

        then

        consider F be Function of the carrier of X, the carrier of X such that

         A10: S c= ( dom F) and

         A11: for y st y in S holds (F . y) = ((x .|. y) * y) by A9;

        set z = ( setopfunc (S,the carrier of X,the carrier of X,F,the addF of X));

        (z .|. x) = ( setopfunc (S,the carrier of X, REAL ,H, addreal )) by A1, A2, A3, A4, A5, A10, A11, Th11;

        then (x .|. z) = (z .|. z) by A1, A2, A3, A4, A5, A10, A11, Th12;

        

        then ((x - z) .|. (x - z)) = ((((x .|. x) - (z .|. z)) - (z .|. z)) + (z .|. z)) by BHSP_1: 13

        .= ((x .|. x) - ( setopfunc (S,the carrier of X, REAL ,H, addreal ))) by A1, A2, A3, A4, A5, A10, A11, Th12;

        hence 0 <= ((x .|. x) - ( setopfunc (S,the carrier of X, REAL ,H, addreal ))) by BHSP_1:def 2;

      end;

      then

       A12: ( 0 + ( setopfunc (S,the carrier of X, REAL ,H, addreal ))) <= (x .|. x) by XREAL_1: 19;

       0 <= (x .|. x) by BHSP_1:def 2;

      then ( setopfunc (S,the carrier of X, REAL ,H, addreal )) <= (( sqrt (x .|. x)) ^2 ) by A12, SQUARE_1:def 2;

      hence thesis by BHSP_1:def 4;

    end;

    theorem :: BHSP_5:14

    for DK,DX be non empty set holds for f be BinOp of DK st f is commutative associative & f is having_a_unity holds for Y1,Y2 be finite Subset of DX st Y1 misses Y2 holds for F be Function of DX, DK st Y1 c= ( dom F) & Y2 c= ( dom F) holds for Z be finite Subset of DX st Z = (Y1 \/ Y2) holds ( setopfunc (Z,DX,DK,F,f)) = (f . (( setopfunc (Y1,DX,DK,F,f)),( setopfunc (Y2,DX,DK,F,f))))

    proof

      let DK,DX be non empty set;

      let f be BinOp of DK such that

       A1: f is commutative associative and

       A2: f is having_a_unity;

      let Y1,Y2 be finite Subset of DX such that

       A3: Y1 misses Y2;

      let F be Function of DX, DK such that

       A4: Y1 c= ( dom F) and

       A5: Y2 c= ( dom F);

      let Z be finite Subset of DX;

      assume

       A6: Z = (Y1 \/ Y2);

      consider p1 be FinSequence of DX such that

       A8: p1 is one-to-one and

       A9: ( rng p1) = Y1 and

       A10: ( setopfunc (Y1,DX,DK,F,f)) = (f "**" ( Func_Seq (F,p1))) by A1, A2, Def5;

      consider p2 be FinSequence of DX such that

       A11: p2 is one-to-one and

       A12: ( rng p2) = Y2 and

       A13: ( setopfunc (Y2,DX,DK,F,f)) = (f "**" ( Func_Seq (F,p2))) by A1, A2, Def5;

      set q = (p1 ^ p2);

      

       A14: q is one-to-one by A3, A8, A9, A11, A12, FINSEQ_3: 91;

      ( rng q) = Z by A6, A9, A12, FINSEQ_1: 31;

      then

       A15: ( setopfunc (Z,DX,DK,F,f)) = (f "**" ( Func_Seq (F,q))) by A1, A2, A14, Def5;

      ex fp1,fp2 be FinSequence st fp1 = (F * p1) & fp2 = (F * p2) & (F * (p1 ^ p2)) = (fp1 ^ fp2) by A4, A5, A6, A9, A12, HILBASIS: 1, XBOOLE_1: 8;

      hence thesis by A1, A2, A10, A13, A15, FINSOP_1: 5;

    end;