cayldick.miz



    begin

    reserve u,v,x,y,z,X,Y for set;

    reserve r,s for Real;

    theorem :: CAYLDICK:1

    

     Th1: for a,b,c,d be Real holds (((a + b) ^2 ) + ((c + d) ^2 )) <= ((( sqrt ((a ^2 ) + (c ^2 ))) + ( sqrt ((b ^2 ) + (d ^2 )))) ^2 )

    proof

      let a,b,c,d be Real;

      set A = ((a ^2 ) + (c ^2 )), B = ((b ^2 ) + (d ^2 )), C1 = ( sqrt A), C2 = ( sqrt B);

      

       A1: 0 <= C1 & 0 <= C2 by SQUARE_1:def 2;

      

       A2: (C1 ^2 ) = A & (C2 ^2 ) = B by SQUARE_1:def 2;

      

       A3: ((((a ^2 ) + ((2 * a) * b)) + (b ^2 )) + (((c ^2 ) + ((2 * c) * d)) + (d ^2 ))) = (((((a ^2 ) + (c ^2 )) + (b ^2 )) + (d ^2 )) + (((2 * a) * b) + ((2 * c) * d)));

      

       A4: ((A + ((2 * C1) * C2)) + B) = ((A + B) + ((2 * C1) * C2));

      

       A5: (((2 * a) * b) + ((2 * c) * d)) = (2 * ((a * b) + (c * d)));

      

       A6: (2 * (C1 * C2)) = ((2 * C1) * C2);

      (((a * d) - (c * b)) ^2 ) = ((((a * d) ^2 ) + ((c * b) ^2 )) - ((2 * (a * d)) * (c * b)));

      then

       A7: ( 0 + ((2 * (a * d)) * (c * b))) <= (((((a * d) ^2 ) + ((c * b) ^2 )) - ((2 * (a * d)) * (c * b))) + ((2 * (a * d)) * (c * b))) by XREAL_1: 6;

      

       A8: (A * B) = (( sqrt (A * B)) ^2 ) by SQUARE_1:def 2;

      ((((a ^2 ) * (b ^2 )) + ((c ^2 ) * (d ^2 ))) + ((((2 * a) * b) * c) * d)) <= ((((a ^2 ) * (b ^2 )) + ((c ^2 ) * (d ^2 ))) + (((c ^2 ) * (b ^2 )) + ((a ^2 ) * (d ^2 )))) by A7, XREAL_1: 6;

      then

       A9: (((a * b) + (c * d)) ^2 ) <= (A * B);

      (C1 * C2) = ( sqrt (A * B)) by SQUARE_1: 29;

      then ((a * b) + (c * d)) <= (C1 * C2) by A1, A8, A9, SQUARE_1: 16;

      then (((2 * a) * b) + ((2 * c) * d)) <= ((2 * C1) * C2) by A5, A6, XREAL_1: 64;

      hence thesis by A2, A3, A4, XREAL_1: 6;

    end;

    registration

      let X be non trivial RealNormSpace;

      let x be non zero Element of X;

      cluster ||.x.|| -> positive;

      coherence

      proof

        x <> ( 0. X);

        then 0 <> ||.x.|| by NORMSP_0:def 5;

        hence thesis;

      end;

    end

    registration

      let c be non zero Complex;

      cluster (c ^2 ) -> non zero;

      coherence by XCMPLX_1: 6;

    end

    registration

      let x be non empty set;

      cluster <%x%> -> non-empty;

      coherence

      proof

        let y be object;

        assume y in ( dom <%x%>);

        then y in 1 by AFINSQ_1:def 4;

        then y = 0 by CARD_1: 49, TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      cluster non-empty for XFinSequence;

      existence

      proof

        take <% the non empty set%>;

        thus thesis;

      end;

    end

    registration

      let f,g be non-empty XFinSequence;

      cluster (f ^ g) -> non-empty;

      coherence

      proof

        

         A1: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by AFINSQ_1: 26;

         not {} in ( rng f) & not {} in ( rng g) by RELAT_1:def 9;

        then not {} in ( rng (f ^ g)) by A1, XBOOLE_0:def 3;

        hence thesis by RELAT_1:def 9;

      end;

    end

    registration

      let x,y be non empty set;

      cluster <%x, y%> -> non-empty;

      coherence ;

    end

    theorem :: CAYLDICK:2

     <%u%> = <%x%> implies u = x

    proof

      ( <%u%> . 0 ) = u & ( <%x%> . 0 ) = x;

      hence thesis;

    end;

    theorem :: CAYLDICK:3

    

     Th3: <%u, v%> = <%x, y%> implies u = x & v = y

    proof

      ( <%u, v%> . 0 ) = u & ( <%u, v%> . 1) = v & ( <%x, y%> . 0 ) = x & ( <%x, y%> . 1) = y;

      hence thesis;

    end;

    theorem :: CAYLDICK:4

    x in X implies <%x%> in ( product <%X%>)

    proof

      set f = <%X%>;

      set g = <%x%>;

      assume

       A1: x in X;

      

       A2: ( len f) = 1 by AFINSQ_1: 34;

      

       A3: ( len g) = ( dom g);

      now

        let a be object;

        assume a in ( dom f);

        then a = 0 by A2, CARD_1: 49, TARSKI:def 1;

        hence (g . a) in (f . a) by A1;

      end;

      hence thesis by A2, A3, CARD_3: 9, AFINSQ_1: 34;

    end;

    theorem :: CAYLDICK:5

    z in ( product <%X%>) implies ex x st x in X & z = <%x%>

    proof

      assume z in ( product <%X%>);

      then

      consider f be Function such that

       A1: z = f and

       A2: ( dom f) = ( dom <%X%>) and

       A3: for x be object st x in ( dom <%X%>) holds (f . x) in ( <%X%> . x) by CARD_3:def 5;

      reconsider f as XFinSequence by A2, AFINSQ_1: 5;

      take (f . 0 );

      

       A4: 0 in { 0 } by TARSKI:def 1;

      

       A5: ( <%X%> . 0 ) = X;

      ( len <%X%>) = 1 by AFINSQ_1: 34;

      then ( len f) = 1 by A2;

      hence thesis by A5, A4, A1, A2, A3, AFINSQ_1: 34, CARD_1: 49;

    end;

    theorem :: CAYLDICK:6

    

     Th6: x in X & y in Y implies <%x, y%> in ( product <%X, Y%>)

    proof

      set f = <%X, Y%>;

      set g = <%x, y%>;

      assume

       A1: x in X & y in Y;

      

       A2: ( len f) = 2 by AFINSQ_1: 38;

      

       A3: ( len g) = ( dom g);

      now

        let a be object;

        assume a in ( dom f);

        then a = 0 or a = 1 by A2, TARSKI:def 2, CARD_1: 50;

        hence (g . a) in (f . a) by A1;

      end;

      hence thesis by A2, A3, CARD_3: 9, AFINSQ_1: 38;

    end;

    theorem :: CAYLDICK:7

    

     Th7: z in ( product <%X, Y%>) implies ex x, y st x in X & y in Y & z = <%x, y%>

    proof

      assume z in ( product <%X, Y%>);

      then

      consider f be Function such that

       A1: z = f and

       A2: ( dom f) = ( dom <%X, Y%>) and

       A3: for x be object st x in ( dom <%X, Y%>) holds (f . x) in ( <%X, Y%> . x) by CARD_3:def 5;

      reconsider f as XFinSequence by A2, AFINSQ_1: 5;

      take (f . 0 ), (f . 1);

      

       A4: 0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

      

       A5: ( <%X, Y%> . 0 ) = X & ( <%X, Y%> . 1) = Y;

      ( len <%X, Y%>) = 2 by AFINSQ_1: 38;

      then ( len f) = 2 by A2;

      hence thesis by A5, A4, A1, A2, A3, AFINSQ_1: 38, CARD_1: 50;

    end;

    definition

      let D be set;

      :: CAYLDICK:def1

      func binop (D) -> BinOp of D equals ( [:D, D:] --> the Element of D);

      coherence

      proof

        per cases ;

          suppose D is non empty;

          then

          reconsider D as non empty set;

          ( [:D, D:] --> the Element of D) is BinOp of D;

          hence thesis;

        end;

          suppose D is empty;

          hence thesis;

        end;

      end;

    end

    registration

      let D be set;

      cluster ( binop D) -> associative commutative;

      coherence

      proof

        set f = ( binop D);

        thus f is associative

        proof

          let a,b,c be Element of D;

          per cases ;

            suppose

             A1: D is non empty;

            

            hence (f . (a,(f . (b,c)))) = the Element of D by ZFMISC_1: 87, FUNCOP_1: 7

            .= (f . ((f . (a,b)),c)) by A1, ZFMISC_1: 87, FUNCOP_1: 7;

          end;

            suppose

             A2: D is empty;

            

            hence (f . (a,(f . (b,c)))) = {}

            .= (f . ((f . (a,b)),c)) by A2;

          end;

        end;

        let a,b be Element of D;

        per cases ;

          suppose

           A3: D is non empty;

          

          hence (f . (a,b)) = the Element of D by ZFMISC_1: 87, FUNCOP_1: 7

          .= (f . (b,a)) by A3, ZFMISC_1: 87, FUNCOP_1: 7;

        end;

          suppose

           A4: D is empty;

          

          hence (f . (a,b)) = {}

          .= (f . (b,a)) by A4;

        end;

      end;

    end

    registration

      let D be set;

      cluster associative commutative for BinOp of D;

      existence

      proof

        take ( binop D);

        thus thesis;

      end;

    end

    begin

    definition

      struct ( Normed_AlgebraStr) ConjNormAlgStr (# the carrier -> set,

the multF, addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the OneF, ZeroF -> Element of the carrier,

the normF -> Function of the carrier, REAL ,

the conjugateF -> Function of the carrier, the carrier #)

       attr strict strict;

    end

    registration

      cluster non trivial strict for ConjNormAlgStr;

      existence

      proof

        set A = the non trivial set;

        take ConjNormAlgStr (# A, the BinOp of A, the BinOp of A, the Function of [: REAL , A:], A, the Element of A, the Element of A, the Function of A, REAL , the Function of A, A #);

        thus thesis;

      end;

    end

    reserve N for non empty ConjNormAlgStr;

    reserve a,a1,a2,b,b1,b2 for Element of N;

    definition

      let N be non empty ConjNormAlgStr;

      let a be Element of N;

      :: CAYLDICK:def2

      func a *' -> Element of N equals (the conjugateF of N . a);

      coherence ;

    end

    definition

      let N be non empty ConjNormAlgStr, a be Element of N;

      :: CAYLDICK:def3

      attr a is well-conjugated means

      : Def3: ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) if a is non zero

      otherwise (a *' ) is zero;

      consistency ;

    end

    definition

      let N be non empty ConjNormAlgStr;

      :: CAYLDICK:def4

      attr N is well-conjugated means

      : Def4: for a be Element of N holds a is well-conjugated;

      :: CAYLDICK:def5

      attr N is add-conjugative means

      : Def5: for a,b be Element of N holds ((a + b) *' ) = ((a *' ) + (b *' ));

      :: CAYLDICK:def6

      attr N is norm-conjugative means

      : Def6: for a be Element of N holds ||.(a *' ).|| = ||.a.||;

      :: CAYLDICK:def7

      attr N is scalar-conjugative means

      : Def7: for r be Real, a be Element of N holds (r * (a *' )) = ((r * a) *' );

    end

    registration

      let D be real-membered set;

      let a,m be BinOp of D;

      let M be Function of [: REAL , D:], D;

      let O,Z be Element of D;

      let n be Function of D, REAL ;

      let c be Function of D, D;

      cluster ConjNormAlgStr (# D, m, a, M, O, Z, n, c #) -> real-membered;

      coherence ;

    end

    registration

      let D be set;

      let a be associative BinOp of D;

      let m be BinOp of D;

      let M be Function of [: REAL , D:], D;

      let O,Z be Element of D;

      let n be Function of D, REAL ;

      let c be Function of D, D;

      cluster ConjNormAlgStr (# D, m, a, M, O, Z, n, c #) -> add-associative;

      coherence by BINOP_1:def 3;

    end

    registration

      let D be set;

      let a be commutative BinOp of D;

      let m be BinOp of D;

      let M be Function of [: REAL , D:], D;

      let O,Z be Element of D;

      let n be Function of D, REAL ;

      let c be Function of D, D;

      cluster ConjNormAlgStr (# D, m, a, M, O, Z, n, c #) -> Abelian;

      coherence by BINOP_1:def 2;

    end

    registration

      let D be set;

      let a be BinOp of D;

      let m be associative BinOp of D;

      let M be Function of [: REAL , D:], D;

      let O,Z be Element of D;

      let n be Function of D, REAL ;

      let c be Function of D, D;

      cluster ConjNormAlgStr (# D, m, a, M, O, Z, n, c #) -> associative;

      coherence by BINOP_1:def 3;

    end

    registration

      let D be set;

      let a be BinOp of D;

      let m be commutative BinOp of D;

      let M be Function of [: REAL , D:], D;

      let O,Z be Element of D;

      let n be Function of D, REAL ;

      let c be Function of D, D;

      cluster ConjNormAlgStr (# D, m, a, M, O, Z, n, c #) -> commutative;

      coherence by BINOP_1:def 2;

    end

    definition

      :: CAYLDICK:def8

      func N_Real -> strict ConjNormAlgStr equals ConjNormAlgStr (# REAL , multreal , addreal , multreal , ( In (1, REAL )), ( In ( 0 , REAL )), absreal , ( id REAL ) #);

      coherence ;

    end

    registration

      cluster N_Real -> non degenerated real-membered add-associative Abelian associative commutative;

      coherence ;

    end

    registration

      let a,b be Element of N_Real ;

      let r,s be Real;

      identify r + s with a + b when a = r, b = s;

      compatibility by BINOP_2:def 9;

      identify r * s with a * b when a = r, b = s;

      compatibility by BINOP_2:def 11;

    end

    registration

      cluster right_add-cancelable -> left_add-cancelable for Abelian non empty addMagma;

      coherence

      proof

        let M be Abelian non empty addMagma;

        assume

         A1: M is right_add-cancelable;

        let x,y,z be Element of M;

        assume (x + y) = (x + z);

        hence thesis by A1, ALGSTR_0:def 4;

      end;

      cluster left_add-cancelable -> right_add-cancelable for Abelian non empty addMagma;

      coherence

      proof

        let M be Abelian non empty addMagma such that

         A2: M is left_add-cancelable;

        let x,y,z be Element of M;

        assume (y + x) = (z + x);

        hence thesis by A2, ALGSTR_0:def 3;

      end;

      cluster left_complementable -> right_complementable for Abelian non empty addLoopStr;

      coherence

      proof

        let M be Abelian non empty addLoopStr such that

         A3: M is left_complementable;

        let x be Element of M;

        ex y be Element of M st (y + x) = ( 0. M) by A3, ALGSTR_0:def 10;

        hence x is right_complementable;

      end;

      cluster left-distributive -> right-distributive for Abelian commutative non empty doubleLoopStr;

      coherence

      proof

        let M be Abelian commutative non empty doubleLoopStr such that

         A4: M is left-distributive;

        let x,y,z be Element of M;

        thus (x * (y + z)) = ((x * y) + (x * z)) by A4;

      end;

      cluster right-distributive -> left-distributive for Abelian commutative non empty doubleLoopStr;

      coherence

      proof

        let M be Abelian commutative non empty doubleLoopStr such that

         A5: M is right-distributive;

        let x,y,z be Element of M;

        thus ((y + z) * x) = ((y * x) + (z * x)) by A5;

      end;

      cluster almost_left_invertible -> almost_right_invertible for commutative non empty multLoopStr_0;

      coherence

      proof

        let M be commutative non empty multLoopStr_0 such that

         A6: M is almost_left_invertible;

        let x be Element of M;

        assume x <> ( 0. M);

        then

        consider y be Element of M such that

         A7: (y * x) = ( 1. M) by A6;

        take y;

        thus thesis by A7;

      end;

      cluster almost_right_invertible -> almost_left_invertible for commutative non empty multLoopStr_0;

      coherence

      proof

        let M be commutative non empty multLoopStr_0 such that

         A8: M is almost_right_invertible;

        let x be Element of M;

        assume x <> ( 0. M);

        then

        consider y be Element of M such that

         A9: (x * y) = ( 1. M) by A8, ALGSTR_0:def 28;

        take y;

        thus thesis by A9;

      end;

      cluster almost_right_cancelable -> almost_left_cancelable for commutative non empty multLoopStr_0;

      coherence

      proof

        let M be commutative non empty multLoopStr_0 such that

         A10: M is almost_right_cancelable;

        let x be Element of M;

        assume

         A11: x <> ( 0. M);

        let y,z be Element of M;

        assume (x * y) = (x * z);

        hence thesis by A10, A11, ALGSTR_0:def 21;

      end;

      cluster almost_left_cancelable -> almost_right_cancelable for commutative non empty multLoopStr_0;

      coherence

      proof

        let M be commutative non empty multLoopStr_0 such that

         A12: M is almost_left_cancelable;

        let x be Element of M;

        assume

         A13: x <> ( 0. M);

        let y,z be Element of M;

        assume (y * x) = (z * x);

        hence thesis by A12, A13, ALGSTR_0:def 20;

      end;

      cluster right_mult-cancelable -> left_mult-cancelable for commutative non empty multMagma;

      coherence

      proof

        let M be commutative non empty multMagma such that

         A14: M is right_mult-cancelable;

        let x,y,z be Element of M;

        assume (x * y) = (x * z);

        hence thesis by A14, ALGSTR_0:def 21;

      end;

      cluster left_mult-cancelable -> right_mult-cancelable for commutative non empty multMagma;

      coherence

      proof

        let M be commutative non empty multMagma such that

         A15: M is left_mult-cancelable;

        let x,y,z be Element of M;

        assume (y * x) = (z * x);

        hence thesis by A15, ALGSTR_0:def 20;

      end;

    end

    registration

      cluster N_Real -> right_complementable right_add-cancelable;

      coherence

      proof

        thus N_Real is right_complementable

        proof

          let a be Element of N_Real ;

          reconsider b = ( - a qua Real) as Element of N_Real by XREAL_0:def 1;

          take b;

          thus thesis;

        end;

        let a be Element of N_Real ;

        thus for b,c be Element of N_Real st (b + a) = (c + a) holds b = c;

      end;

    end

    registration

      let a be Element of N_Real ;

      let r be Real;

      identify - r with - a when a = r;

      compatibility

      proof

        assume

         A1: a = r;

        reconsider b = ( - r) as Element of N_Real by XREAL_0:def 1;

        (b + a) = ( 0. N_Real ) by A1;

        hence thesis by ALGSTR_0:def 13;

      end;

    end

    registration

      let a,b be Element of N_Real ;

      let r,s be Real;

      identify r - s with a - b when a = r, b = s;

      compatibility ;

    end

    registration

      let a be Element of N_Real ;

      let r,s be Real;

      identify r * s with r * a when a = s;

      compatibility by BINOP_2:def 11;

    end

    registration

      let a be Element of N_Real ;

      identify |.a.| with ||.a.||;

      compatibility by EUCLID:def 2;

    end

    theorem :: CAYLDICK:8

    

     Th8: for a be Element of N_Real holds (a * a) = ( ||.a.|| ^2 )

    proof

      let a be Element of N_Real ;

      reconsider x = a as Element of REAL ;

      

      thus (a * a) = (x ^2 )

      .= ( ||.a.|| ^2 ) by COMPLEX1: 75;

    end;

    registration

      let a be Element of N_Real ;

      reduce (a *' ) to a;

      reducibility ;

    end

    registration

      cluster N_Real -> reflexive discerning well-unital RealNormSpace-like right_zeroed right-distributive vector-associative vector-distributive scalar-distributive scalar-associative scalar-unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 almost_left_invertible almost_left_cancelable well-conjugated add-conjugative norm-conjugative scalar-conjugative;

      coherence

      proof

        thus ||.( 0. N_Real ).|| = 0 ;

        thus for a be Element of N_Real st ||.a.|| = 0 holds a = ( 0. N_Real );

        thus for a be Element of N_Real holds (a * ( 1. N_Real )) = a & (( 1. N_Real ) * a) = a;

        thus for a,b be Element of N_Real , r holds ||.(r * a).|| = ( |.r.| * ||.a.||) & ||.(a + b).|| <= ( ||.a.|| + ||.b.||) by COMPLEX1: 56, COMPLEX1: 65;

        thus for a be Element of N_Real holds (a + ( 0. N_Real )) = a;

        thus for a,b,c be Element of N_Real holds (a * (b + c)) = ((a * b) + (a * c));

        thus for a,b be Element of N_Real holds for r holds (r * (a * b)) = ((r * a) * b);

        thus for r holds for a,b be Element of N_Real holds (r * (a + b)) = ((r * a) + (r * b));

        thus for r, s holds for a be Element of N_Real holds ((r + s) * a) = ((r * a) + (s * a));

        thus for r, s holds for a be Element of N_Real holds ((r * s) * a) = (r * (s * a));

        thus for a be Element of N_Real holds (1 * a) = a;

        thus for a,b be Element of N_Real holds ||.(a * b).|| <= ( ||.a.|| * ||.b.||) by COMPLEX1: 65;

        thus ||.( 1. N_Real ).|| = 1 by COMPLEX1: 43;

        thus for r holds for a,b be Element of N_Real holds (r * (a * b)) = (a * (r * b));

        thus for a be Element of N_Real st a <> ( 0. N_Real ) holds ex b be Element of N_Real st (b * a) = ( 1. N_Real )

        proof

          let a be Element of N_Real such that

           A1: a <> ( 0. N_Real );

          reconsider b = (a qua Real " ) as Element of N_Real by XREAL_0:def 1;

          take b;

          thus thesis by A1, XCMPLX_0:def 7;

        end;

        thus for a be Element of N_Real st a <> ( 0. N_Real ) holds a is left_mult-cancelable by XCMPLX_1: 5;

        thus N_Real is well-conjugated

        proof

          let a be Element of N_Real ;

          per cases ;

            case a is non zero;

            thus ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N_Real )) by Th8;

          end;

            case a is zero;

            hence (a *' ) = ( 0. N_Real );

          end;

        end;

        thus for a,b be Element of N_Real holds ((a + b) *' ) = ((a *' ) + (b *' ));

        thus for a be Element of N_Real holds ||.(a *' ).|| = ||.a.||;

        thus for r holds for a be Element of N_Real holds (r * (a *' )) = ((r * a) *' );

      end;

    end

    registration

      cluster strict non degenerated real-membered reflexive discerning zeroed complementable add-associative Abelian associative commutative distributive well-unital add-cancelable vector-associative vector-distributive scalar-distributive scalar-associative scalar-unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 well-conjugated add-conjugative norm-conjugative scalar-conjugative almost_left_invertible almost_left_cancelable RealNormSpace-like for non empty ConjNormAlgStr;

      existence

      proof

        take N_Real ;

        thus thesis;

      end;

    end

    registration

      cluster ( 0. N_Real ) -> non left_invertible non right_invertible;

      coherence ;

    end

    registration

      let a be non zero Element of N_Real ;

      let r be Real;

      identify r " with a " when a = r;

      compatibility

      proof

        assume

         A1: a = r;

        reconsider b = (r " ) as Element of N_Real by XREAL_0:def 1;

        

         A2: a <> ( 0. N_Real );

        then (b * a) = ( 1. N_Real ) by A1, XCMPLX_0:def 7;

        hence thesis by A2, VECTSP_2:def 2;

      end;

    end

    registration

      let X be discerning non trivial ConjNormAlgStr;

      let x be non zero Element of X;

      cluster ||.x.|| -> non zero;

      coherence

      proof

        x <> ( 0. X);

        hence thesis by NORMSP_0:def 5;

      end;

    end

    registration

      cluster -> non empty for non zero Element of N_Real ;

      coherence

      proof

        let a be non zero Element of N_Real ;

        ( 0. N_Real ) = 0 ;

        hence thesis;

      end;

    end

    registration

      cluster -> mult-cancelable for non zero Element of N_Real ;

      coherence

      proof

        let x be non zero Element of N_Real ;

        thus x is right_mult-cancelable by XCMPLX_1: 5;

        let y,z be Element of N_Real ;

        thus thesis by XCMPLX_1: 5;

      end;

    end

    registration

      let N be well-conjugated non empty ConjNormAlgStr;

      cluster -> well-conjugated for Element of N;

      coherence by Def4;

    end

    registration

      let N be well-conjugated non empty ConjNormAlgStr;

      let a be zero Element of N;

      cluster (a *' ) -> zero;

      coherence by Def3;

    end

    registration

      let N be well-conjugated non empty ConjNormAlgStr;

      reduce (( 0. N) *' ) to ( 0. N);

      reducibility by STRUCT_0:def 12;

    end

    registration

      let N be well-conjugated discerning add-associative right_zeroed right_complementable left-distributive scalar-distributive scalar-associative scalar-unital vector-distributive non degenerated ConjNormAlgStr;

      let a be non zero Element of N;

      cluster (a *' ) -> non zero;

      coherence

      proof

        assume (a *' ) is zero;

        then

         A1: (a *' ) = ( 0. N);

        ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) by Def3;

        hence thesis by A1, RLVECT_1: 11;

      end;

    end

    theorem :: CAYLDICK:9

    

     Th9: N is add-associative right_zeroed right_complementable well-conjugated reflexive scalar-distributive scalar-unital vector-distributive left-distributive implies for a holds ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N))

    proof

      assume that

       A1: N is add-associative right_zeroed right_complementable and

       A2: N is well-conjugated and

       A3: N is reflexive and

       A4: N is scalar-distributive scalar-unital vector-distributive left-distributive;

      let a;

      per cases ;

        suppose a is non zero;

        hence ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) by A2, Def3;

      end;

        suppose

         A5: a is zero;

        then

         A6: a = ( 0. N) & (a *' ) = ( 0. N) by A2;

        

         A7: ( ||.a.|| ^2 ) = 0 by A3, A5;

        ( 0 * ( 1. N)) = ( 0. N) by A1, A4, RLVECT_1: 10;

        hence thesis by A1, A6, A4, A7;

      end;

    end;

    registration

      let N be well-conjugated reflexive discerning add-associative right_zeroed right_complementable almost_right_cancelable associative commutative well-unital almost_left_invertible distributive scalar-distributive scalar-associative scalar-unital vector-distributive norm-conjugative non degenerated ConjNormAlgStr;

      let a be Element of N;

      reduce ((a *' ) *' ) to a;

      reducibility

      proof

        per cases ;

          suppose

           A1: a is non zero;

          then

           A2: ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) by Def3;

          

           A3: (((a *' ) *' ) * (a *' )) = (( ||.(a *' ).|| ^2 ) * ( 1. N)) by A1, Def3;

          

           A4: ||.(a *' ).|| = ||.a.|| by Def6;

          (a *' ) <> ( 0. N) by A1;

          hence thesis by A2, A3, A4, ALGSTR_0:def 21, ALGSTR_0:def 37;

        end;

          suppose a is zero;

          then a = ( 0. N);

          hence thesis;

        end;

      end;

    end

    

     Lm1: (N is left_unital or N is right_unital) & N is Banach_Algebra-like_2 almost_right_cancelable well-conjugated scalar-unital implies (( 1. N) *' ) = ( 1. N)

    proof

      assume that

       A1: N is left_unital or N is right_unital and

       A2: N is Banach_Algebra-like_2 and

       A3: N is almost_right_cancelable and

       A4: N is well-conjugated and

       A5: N is scalar-unital;

      per cases ;

        suppose

         A6: ( 1. N) is non zero;

        then

         A7: ( 1. N) <> ( 0. N);

        

         A8: ||.( 1. N).|| = 1 by A2;

        ((( 1. N) *' ) * ( 1. N)) = (( ||.( 1. N).|| ^2 ) * ( 1. N)) by A4, A6, Def3

        .= ( 1. N) by A8, A5

        .= (( 1. N) * ( 1. N)) by A1;

        hence thesis by A3, A7, ALGSTR_0:def 21;

      end;

        suppose ( 1. N) is zero;

        then ( 1. N) = (( 0. N) *' ) by A4;

        hence thesis by A4;

      end;

    end;

    registration

      let N be left_unital Banach_Algebra-like_2 almost_right_cancelable well-conjugated scalar-unital non empty ConjNormAlgStr;

      reduce (( 1. N) *' ) to ( 1. N);

      reducibility by Lm1;

    end

    registration

      let N be right_unital Banach_Algebra-like_2 almost_right_cancelable well-conjugated scalar-unital non empty ConjNormAlgStr;

      reduce (( 1. N) *' ) to ( 1. N);

      reducibility by Lm1;

    end

    theorem :: CAYLDICK:10

    

     Th10: N is well-conjugated reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable associative distributive well-unital non degenerated almost_left_invertible implies (( - a) *' ) = ( - (a *' ))

    proof

      assume that

       A1: N is well-conjugated and

       A2: N is reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable and

       A3: N is associative and

       A4: N is distributive and

       A5: N is well-unital and

       A6: N is non degenerated almost_left_invertible;

      per cases ;

        suppose

         A7: a is non zero;

        then

         A8: ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) by A1, Def3;

        

         A9: ((( - a) *' ) * ( - a)) = (( ||.( - a).|| ^2 ) * ( 1. N)) by A1, A2, A6, A7, Def3;

        

         A10: ||.( - a).|| = ||.a.|| by A2, NORMSP_1: 2;

        

         A11: a <> ( 0. N) by A7;

        

         A12: (a * ( / a)) = ( 1. N) by A2, A3, A4, A5, A6, A11, VECTSP_2: 9;

        then

         A13: (( - a) * ( - ( / a))) = ( 1. N) by A2, A4, VECTSP_1: 10;

        

         A14: (a * ( - ( / a))) = ( - ( 1. N)) by A2, A4, A12, VECTSP_1: 8;

        

        thus (( - a) *' ) = ((( - a) *' ) * ( 1. N)) by A5

        .= (((( - a) *' ) * ( - a)) * ( - ( / a))) by A13, A3

        .= ((a *' ) * (a * ( - ( / a)))) by A8, A9, A10, A3

        .= ( - (a *' )) by A2, A14, A4, A5, VECTSP_2: 28;

      end;

        suppose a is zero;

        then

         A15: a = ( 0. N) & (a *' ) = ( 0. N) by A1;

        ( - ( 0. N)) = ( 0. N) by A2;

        hence thesis by A15;

      end;

    end;

    theorem :: CAYLDICK:11

    N is well-conjugated reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable associative distributive well-unital non degenerated almost_left_invertible add-conjugative implies ((a - b) *' ) = ((a *' ) - (b *' ))

    proof

      assume that

       A1: N is well-conjugated reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable associative distributive well-unital non degenerated almost_left_invertible;

      assume N is add-conjugative;

      

      hence ((a - b) *' ) = ((a *' ) + (( - b) *' ))

      .= ((a *' ) - (b *' )) by A1, Th10;

    end;

    begin

    definition

      let N be non empty ConjNormAlgStr;

      :: CAYLDICK:def9

      func Cayley-Dickson (N) -> strict ConjNormAlgStr means

      : Def9: the carrier of it = ( product <%the carrier of N, the carrier of N%>) & the ZeroF of it = <%( 0. N), ( 0. N)%> & the OneF of it = <%( 1. N), ( 0. N)%> & (for a1,a2,b1,b2 be Element of N holds (the addF of it . ( <%a1, b1%>, <%a2, b2%>)) = <%(a1 + a2), (b1 + b2)%> & (the multF of it . ( <%a1, b1%>, <%a2, b2%>)) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%>) & (for r be Real, a,b be Element of N holds (the Mult of it . (r, <%a, b%>)) = <%(r * a), (r * b)%>) & for a,b be Element of N holds (the normF of it . <%a, b%>) = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) & (the conjugateF of it . <%a, b%>) = <%(a *' ), ( - b)%>;

      existence

      proof

        set A = the carrier of N;

        set C = ( product <%A, A%>);

        defpred A[ Element of C, Element of C, set] means ex a1,a2,b1,b2 be Element of N st $1 = <%a1, b1%> & $2 = <%a2, b2%> & $3 = <%(a1 + a2), (b1 + b2)%>;

        

         A1: for x,y be Element of C holds ex z be Element of C st A[x, y, z]

        proof

          let a,b be Element of C;

          consider a1,b1 be set such that

           A2: a1 in A & b1 in A and

           A3: a = <%a1, b1%> by Th7;

          consider a2,b2 be set such that

           A4: a2 in A & b2 in A and

           A5: b = <%a2, b2%> by Th7;

          reconsider a1, a2, b1, b2 as Element of A by A2, A4;

          take c = <%(a1 + a2), (b1 + b2)%>;

          thus c is Element of C by Th6;

          thus thesis by A3, A5;

        end;

        consider add be Function of [:C, C:], C such that

         A6: for x,y be Element of C holds A[x, y, (add . (x,y))] from BINOP_1:sch 3( A1);

        defpred M[ Element of C, Element of C, set] means ex a1,a2,b1,b2 be Element of N st $1 = <%a1, b1%> & $2 = <%a2, b2%> & $3 = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%>;

        

         A7: for x,y be Element of C holds ex z be Element of C st M[x, y, z]

        proof

          let a,b be Element of C;

          consider a1,b1 be set such that

           A8: a1 in A & b1 in A and

           A9: a = <%a1, b1%> by Th7;

          consider a2,b2 be set such that

           A10: a2 in A & b2 in A and

           A11: b = <%a2, b2%> by Th7;

          reconsider a1, a2, b1, b2 as Element of A by A8, A10;

          take z = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%>;

          thus z is Element of C by Th6;

          thus thesis by A9, A11;

        end;

        consider mult be Function of [:C, C:], C such that

         A12: for x,y be Element of C holds M[x, y, (mult . (x,y))] from BINOP_1:sch 3( A7);

        defpred MU[ Element of REAL , Element of C, set] means ex a,b be Element of N st $2 = <%a, b%> & $3 = <%($1 * a), ($1 * b)%>;

        

         A13: for x be Element of REAL , y be Element of C holds ex z be Element of C st MU[x, y, z]

        proof

          let r be Element of REAL , c be Element of C;

          consider a,b be set such that

           A14: a in A & b in A and

           A15: c = <%a, b%> by Th7;

          reconsider a, b as Element of A by A14;

          take z = <%(r * a), (r * b)%>;

          thus z is Element of C by Th6;

          thus thesis by A15;

        end;

        consider MU be Function of [: REAL , C:], C such that

         A16: for x be Element of REAL , y be Element of C holds MU[x, y, (MU . (x,y))] from BINOP_1:sch 3( A13);

        defpred N[ Element of C, set] means ex a,b be Element of N st $1 = <%a, b%> & $2 = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 )));

        

         A17: for x be Element of C holds ex y be Element of REAL st N[x, y]

        proof

          let c be Element of C;

          consider a,b be set such that

           A18: a in A & b in A and

           A19: c = <%a, b%> by Th7;

          reconsider a, b as Element of A by A18;

          take ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 )));

          thus thesis by A19, XREAL_0:def 1, TARSKI: 1;

        end;

        consider norm be Function of C, REAL such that

         A20: for x be Element of C holds N[x, (norm . x)] from FUNCT_2:sch 3( A17);

        defpred C[ Element of C, set] means ex a,b be Element of N st $1 = <%a, b%> & $2 = <%(a *' ), ( - b)%>;

        

         A21: for x be Element of C holds ex y be Element of C st C[x, y]

        proof

          let c be Element of C;

          consider a,b be set such that

           A22: a in A & b in A and

           A23: c = <%a, b%> by Th7;

          reconsider a, b as Element of A by A22;

          take <%(a *' ), ( - b)%>;

          thus thesis by A23, Th6;

        end;

        consider conj be Function of C, C such that

         A24: for x be Element of C holds C[x, (conj . x)] from FUNCT_2:sch 3( A21);

        reconsider Z = <%( 0. N), ( 0. N)%>, O = <%( 1. N), ( 0. N)%> as Element of C by Th6;

        take X = ConjNormAlgStr (# C, mult, add, MU, O, Z, norm, conj #);

        thus the carrier of X = C & the ZeroF of X = <%( 0. N), ( 0. N)%> & the OneF of X = <%( 1. N), ( 0. N)%>;

        hereby

          let a1,a2,b1,b2 be Element of N;

          reconsider a = <%a1, b1%>, b = <%a2, b2%> as Element of C by Th6;

          consider x1,x2,y1,y2 be Element of N such that

           A25: a = <%x1, y1%> & b = <%x2, y2%> and

           A26: (add . (a,b)) = <%(x1 + x2), (y1 + y2)%> by A6;

          a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 by A25, Th3;

          hence (the addF of X . ( <%a1, b1%>, <%a2, b2%>)) = <%(a1 + a2), (b1 + b2)%> by A26;

          consider x1,x2,y1,y2 be Element of N such that

           A27: a = <%x1, y1%> & b = <%x2, y2%> and

           A28: (mult . (a,b)) = <%((x1 * x2) - ((y2 *' ) * y1)), ((y2 * x1) + (y1 * (x2 *' )))%> by A12;

          a1 = x1 & a2 = x2 & b1 = y1 & b2 = y2 by A27, Th3;

          hence (the multF of X . ( <%a1, b1%>, <%a2, b2%>)) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> by A28;

        end;

        hereby

          let r be Real, a,b be Element of N;

          reconsider c = <%a, b%> as Element of C by Th6;

          r in REAL by XREAL_0:def 1;

          then

          consider x,y be Element of N such that

           A29: c = <%x, y%> and

           A30: (MU . (r,c)) = <%(r * x), (r * y)%> by A16;

          a = x & b = y by A29, Th3;

          hence (the Mult of X . (r, <%a, b%>)) = <%(r * a), (r * b)%> by A30;

        end;

        hereby

          let a,b be Element of N;

          reconsider c = <%a, b%> as Element of C by Th6;

          consider x,y be Element of N such that

           A31: c = <%x, y%> and

           A32: (norm . c) = ( sqrt (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))) by A20;

          a = x & b = y by A31, Th3;

          hence (the normF of X . <%a, b%>) = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) by A32;

          consider x,y be Element of N such that

           A33: c = <%x, y%> and

           A34: (conj . c) = <%(x *' ), ( - y)%> by A24;

          a = x & b = y by A33, Th3;

          hence (the conjugateF of X . <%a, b%>) = <%(a *' ), ( - b)%> by A34;

        end;

      end;

      uniqueness

      proof

        let X,Y be strict ConjNormAlgStr such that

         A35: the carrier of X = ( product <%the carrier of N, the carrier of N%>) and

         A36: the ZeroF of X = <%( 0. N), ( 0. N)%> and

         A37: the OneF of X = <%( 1. N), ( 0. N)%> and

         A38: for a1,a2,b1,b2 be Element of N holds (the addF of X . ( <%a1, b1%>, <%a2, b2%>)) = <%(a1 + a2), (b1 + b2)%> & (the multF of X . ( <%a1, b1%>, <%a2, b2%>)) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> and

         A39: for r be Real, a,b be Element of N holds (the Mult of X . (r, <%a, b%>)) = <%(r * a), (r * b)%> and

         A40: for a,b be Element of N holds (the normF of X . <%a, b%>) = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) & (the conjugateF of X . <%a, b%>) = <%(a *' ), ( - b)%> and

         A41: the carrier of Y = ( product <%the carrier of N, the carrier of N%>) and

         A42: the ZeroF of Y = <%( 0. N), ( 0. N)%> and

         A43: the OneF of Y = <%( 1. N), ( 0. N)%> and

         A44: for a1,a2,b1,b2 be Element of N holds (the addF of Y . ( <%a1, b1%>, <%a2, b2%>)) = <%(a1 + a2), (b1 + b2)%> & (the multF of Y . ( <%a1, b1%>, <%a2, b2%>)) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> and

         A45: for r be Real, a,b be Element of N holds (the Mult of Y . (r, <%a, b%>)) = <%(r * a), (r * b)%> and

         A46: for a,b be Element of N holds (the normF of Y . <%a, b%>) = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) & (the conjugateF of Y . <%a, b%>) = <%(a *' ), ( - b)%>;

        

         A47: the addF of X = the addF of Y

        proof

          ( dom the addF of X) = [:the carrier of X, the carrier of X:] by A35, FUNCT_2:def 1;

          hence ( dom the addF of X) = ( dom the addF of Y) by A35, A41, FUNCT_2:def 1;

          let z be object;

          assume z in ( dom the addF of X);

          then

          consider z1,z2 be object such that

           A48: z1 in the carrier of X and

           A49: z2 in the carrier of X and

           A50: z = [z1, z2] by ZFMISC_1:def 2;

          consider a1,b1 be set such that

           A51: a1 in the carrier of N & b1 in the carrier of N and

           A52: z1 = <%a1, b1%> by A35, A48, Th7;

          consider a2,b2 be set such that

           A53: a2 in the carrier of N & b2 in the carrier of N and

           A54: z2 = <%a2, b2%> by A35, A49, Th7;

          reconsider a1, a2, b1, b2 as Element of N by A51, A53;

          

          thus (the addF of X . z) = (the addF of X . (z1,z2)) by A50

          .= <%(a1 + a2), (b1 + b2)%> by A52, A54, A38

          .= (the addF of Y . (z1,z2)) by A52, A54, A44

          .= (the addF of Y . z) by A50;

        end;

        

         A55: the multF of X = the multF of Y

        proof

          ( dom the multF of X) = [:the carrier of X, the carrier of X:] by A35, FUNCT_2:def 1;

          hence ( dom the multF of X) = ( dom the multF of Y) by A35, A41, FUNCT_2:def 1;

          let z be object;

          assume z in ( dom the multF of X);

          then

          consider z1,z2 be object such that

           A56: z1 in the carrier of X and

           A57: z2 in the carrier of X and

           A58: z = [z1, z2] by ZFMISC_1:def 2;

          consider a1,b1 be set such that

           A59: a1 in the carrier of N & b1 in the carrier of N and

           A60: z1 = <%a1, b1%> by A35, A56, Th7;

          consider a2,b2 be set such that

           A61: a2 in the carrier of N & b2 in the carrier of N and

           A62: z2 = <%a2, b2%> by A35, A57, Th7;

          reconsider a1, a2, b1, b2 as Element of N by A59, A61;

          

          thus (the multF of X . z) = (the multF of X . (z1,z2)) by A58

          .= <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> by A60, A62, A38

          .= (the multF of Y . (z1,z2)) by A60, A62, A44

          .= (the multF of Y . z) by A58;

        end;

        

         A63: the Mult of X = the Mult of Y

        proof

          ( dom the Mult of X) = [: REAL , the carrier of X:] by A35, FUNCT_2:def 1;

          hence ( dom the Mult of X) = ( dom the Mult of Y) by A35, A41, FUNCT_2:def 1;

          let z be object;

          assume z in ( dom the Mult of X);

          then

          consider z1,z2 be object such that

           A64: z1 in REAL and

           A65: z2 in the carrier of X and

           A66: z = [z1, z2] by ZFMISC_1:def 2;

          consider a,b be set such that

           A67: a in the carrier of N & b in the carrier of N and

           A68: z2 = <%a, b%> by A35, A65, Th7;

          reconsider z1 as Element of REAL by A64;

          reconsider a, b as Element of N by A67;

          

          thus (the Mult of X . z) = (the Mult of X . (z1,z2)) by A66

          .= <%(z1 * a), (z1 * b)%> by A68, A39

          .= (the Mult of Y . (z1,z2)) by A68, A45

          .= (the Mult of Y . z) by A66;

        end;

        

         A69: the normF of X = the normF of Y

        proof

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

          hence ( dom the normF of X) = ( dom the normF of Y) by A35, A41, FUNCT_2:def 1;

          let z be object;

          assume z in ( dom the normF of X);

          then

          consider a,b be set such that

           A70: a in the carrier of N & b in the carrier of N and

           A71: z = <%a, b%> by A35, Th7;

          reconsider a, b as Element of N by A70;

          

          thus (the normF of X . z) = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) by A71, A40

          .= (the normF of Y . z) by A71, A46;

        end;

        the conjugateF of X = the conjugateF of Y

        proof

          ( dom the conjugateF of X) = the carrier of X by A35, FUNCT_2:def 1;

          hence ( dom the conjugateF of X) = ( dom the conjugateF of Y) by A35, A41, FUNCT_2:def 1;

          let z be object;

          assume z in ( dom the conjugateF of X);

          then

          consider a,b be set such that

           A72: a in the carrier of N & b in the carrier of N and

           A73: z = <%a, b%> by A35, Th7;

          reconsider a, b as Element of N by A72;

          

          thus (the conjugateF of X . z) = <%(a *' ), ( - b)%> by A73, A40

          .= (the conjugateF of Y . z) by A73, A46;

        end;

        hence thesis by A35, A36, A37, A41, A42, A43, A47, A55, A63, A69;

      end;

    end

    reserve c,c1,c2 for Element of ( Cayley-Dickson N);

    registration

      let N be non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> non empty;

      coherence

      proof

        ( product <%the carrier of N, the carrier of N%>) is non empty;

        hence the carrier of ( Cayley-Dickson N) is non empty by Def9;

      end;

    end

    theorem :: CAYLDICK:12

    

     Th12: ex a,b be Element of N st c = <%a, b%>

    proof

      set C = ( Cayley-Dickson N);

      the carrier of C = ( product <%the carrier of N, the carrier of N%>) by Def9;

      then ex a,b be set st a in the carrier of N & b in the carrier of N & c = <%a, b%> by Th7;

      hence thesis;

    end;

    theorem :: CAYLDICK:13

    

     Th13: for c be Element of ( Cayley-Dickson ( Cayley-Dickson N)) holds ex a1, b1, a2, b2 st c = <% <%a1, b1%>, <%a2, b2%>%>

    proof

      let c be Element of ( Cayley-Dickson ( Cayley-Dickson N));

      consider a,b be Element of ( Cayley-Dickson N) such that

       A1: c = <%a, b%> by Th12;

      consider a1,b1 be Element of N such that

       A2: a = <%a1, b1%> by Th12;

      consider a2,b2 be Element of N such that

       A3: b = <%a2, b2%> by Th12;

      take a1, b1, a2, b2;

      thus c = <% <%a1, b1%>, <%a2, b2%>%> by A1, A2, A3;

    end;

    definition

      let N, a, b;

      :: original: <%

      redefine

      func <%a,b%> -> Element of ( Cayley-Dickson N) ;

      coherence

      proof

         <%a, b%> in ( product <%the carrier of N, the carrier of N%>) by Th6;

        hence thesis by Def9;

      end;

    end

    registration

      let N;

      let a,b be zero Element of N;

      cluster <%a, b%> -> zero;

      coherence

      proof

        

         A1: a = ( 0. N) & b = ( 0. N) by STRUCT_0:def 12;

        ( 0. ( Cayley-Dickson N)) = <%( 0. N), ( 0. N)%> by Def9;

        hence thesis by A1;

      end;

    end

    registration

      let N be non degenerated non empty ConjNormAlgStr;

      let a be non zero Element of N;

      let b be Element of N;

      cluster <%a, b%> -> non zero;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        now

          assume <%a, b%> is zero;

          then

           A1: <%a, b%> = ( 0. C);

          ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

          hence contradiction by A1, Th3;

        end;

        hence thesis;

      end;

    end

    registration

      let N be reflexive non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> reflexive;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        

        hence ||.( 0. C).|| = ( sqrt (( ||.( 0. N).|| ^2 ) + ( ||.( 0. N).|| ^2 ))) by Def9

        .= 0 ;

      end;

    end

    registration

      let N be discerning non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> discerning;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C such that

         A1: ||.a.|| = 0 ;

        consider a1,b1 be Element of N such that

         A2: a = <%a1, b1%> by Th12;

         ||.a.|| = ( sqrt (( ||.a1.|| ^2 ) + ( ||.b1.|| ^2 ))) by A2, Def9;

        then ||.a1.|| = 0 & ||.b1.|| = 0 by A1, SQUARE_1: 24;

        then a1 = ( 0. N) & b1 = ( 0. N) by NORMSP_0:def 5;

        hence a = ( 0. C) by A2, Def9;

      end;

    end

    theorem :: CAYLDICK:14

    

     Th14: a is left_complementable & b is left_complementable implies <%a, b%> is left_complementable

    proof

      given x be Element of N such that

       A1: (x + a) = ( 0. N);

      given y be Element of N such that

       A2: (y + b) = ( 0. N);

      take <%x, y%>;

      

      thus ( <%x, y%> + <%a, b%>) = <%(x + a), (y + b)%> by Def9

      .= ( 0. ( Cayley-Dickson N)) by A1, A2, Def9;

    end;

    theorem :: CAYLDICK:15

    

     Th15: <%a, b%> is left_complementable implies a is left_complementable & b is left_complementable

    proof

      set C = ( Cayley-Dickson N);

      given x be Element of C such that

       A1: (x + <%a, b%>) = ( 0. C);

      consider x1,x2 be Element of N such that

       A2: x = <%x1, x2%> by Th12;

      

       A3: ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

      

       A4: ( <%x1, x2%> + <%a, b%>) = <%(x1 + a), (x2 + b)%> by Def9;

      hereby

        take x1;

        thus (x1 + a) = ( 0. N) by A1, A2, A3, A4, Th3;

      end;

      take x2;

      thus (x2 + b) = ( 0. N) by A1, A2, A3, A4, Th3;

    end;

    theorem :: CAYLDICK:16

    

     Th16: a is right_complementable & b is right_complementable implies <%a, b%> is right_complementable

    proof

      given x be Element of N such that

       A1: (a + x) = ( 0. N);

      given y be Element of N such that

       A2: (b + y) = ( 0. N);

      take <%x, y%>;

      

      thus ( <%a, b%> + <%x, y%>) = <%(a + x), (b + y)%> by Def9

      .= ( 0. ( Cayley-Dickson N)) by A1, A2, Def9;

    end;

    theorem :: CAYLDICK:17

    

     Th17: <%a, b%> is right_complementable implies a is right_complementable & b is right_complementable

    proof

      set C = ( Cayley-Dickson N);

      given x be Element of C such that

       A1: ( <%a, b%> + x) = ( 0. C);

      consider x1,x2 be Element of N such that

       A2: x = <%x1, x2%> by Th12;

      

       A3: ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

      

       A4: ( <%a, b%> + <%x1, x2%>) = <%(a + x1), (b + x2)%> by Def9;

      hereby

        take x1;

        thus (a + x1) = ( 0. N) by A1, A2, A3, A4, Th3;

      end;

      take x2;

      thus (b + x2) = ( 0. N) by A1, A2, A3, A4, Th3;

    end;

    theorem :: CAYLDICK:18

    a is complementable & b is complementable implies <%a, b%> is complementable by Th14, Th16;

    theorem :: CAYLDICK:19

     <%a, b%> is complementable implies a is complementable & b is complementable by Th15, Th17;

    theorem :: CAYLDICK:20

    

     Th20: a is left_add-cancelable & b is left_add-cancelable implies <%a, b%> is left_add-cancelable

    proof

      assume

       A1: a is left_add-cancelable & b is left_add-cancelable;

      let y,z be Element of ( Cayley-Dickson N) such that

       A2: ( <%a, b%> + y) = ( <%a, b%> + z);

      consider y1,y2 be Element of N such that

       A3: y = <%y1, y2%> by Th12;

      consider z1,z2 be Element of N such that

       A4: z = <%z1, z2%> by Th12;

      ( <%a, b%> + <%y1, y2%>) = <%(a + y1), (b + y2)%> & ( <%a, b%> + <%z1, z2%>) = <%(a + z1), (b + z2)%> by Def9;

      then (a + y1) = (a + z1) & (b + y2) = (b + z2) by A2, A3, A4, Th3;

      then y1 = z1 & y2 = z2 by A1;

      hence y = z by A3, A4;

    end;

    theorem :: CAYLDICK:21

    

     Th21: <%a, b%> is left_add-cancelable implies a is left_add-cancelable & b is left_add-cancelable

    proof

      assume

       A1: <%a, b%> is left_add-cancelable;

      hereby

        let y,z be Element of N such that

         A2: (a + y) = (a + z);

        ( <%a, b%> + <%y, ( 0. N)%>) = <%(a + y), (b + ( 0. N))%> by Def9

        .= ( <%a, b%> + <%z, ( 0. N)%>) by A2, Def9;

        then <%y, ( 0. N)%> = <%z, ( 0. N)%> by A1;

        hence y = z by Th3;

      end;

      let y,z be Element of N such that

       A3: (b + y) = (b + z);

      ( <%a, b%> + <%( 0. N), y%>) = <%(a + ( 0. N)), (b + y)%> by Def9

      .= ( <%a, b%> + <%( 0. N), z%>) by A3, Def9;

      then <%( 0. N), y%> = <%( 0. N), z%> by A1;

      hence y = z by Th3;

    end;

    theorem :: CAYLDICK:22

    

     Th22: a is right_add-cancelable & b is right_add-cancelable implies <%a, b%> is right_add-cancelable

    proof

      assume

       A1: a is right_add-cancelable & b is right_add-cancelable;

      let y,z be Element of ( Cayley-Dickson N) such that

       A2: (y + <%a, b%>) = (z + <%a, b%>);

      consider y1,y2 be Element of N such that

       A3: y = <%y1, y2%> by Th12;

      consider z1,z2 be Element of N such that

       A4: z = <%z1, z2%> by Th12;

      ( <%y1, y2%> + <%a, b%>) = <%(y1 + a), (y2 + b)%> & ( <%z1, z2%> + <%a, b%>) = <%(z1 + a), (z2 + b)%> by Def9;

      then (y1 + a) = (z1 + a) & (y2 + b) = (z2 + b) by A2, A3, A4, Th3;

      then y1 = z1 & y2 = z2 by A1;

      hence y = z by A3, A4;

    end;

    theorem :: CAYLDICK:23

    

     Th23: <%a, b%> is right_add-cancelable implies a is right_add-cancelable & b is right_add-cancelable

    proof

      assume

       A1: <%a, b%> is right_add-cancelable;

      hereby

        let y,z be Element of N such that

         A2: (y + a) = (z + a);

        ( <%y, ( 0. N)%> + <%a, b%>) = <%(y + a), (( 0. N) + b)%> by Def9

        .= ( <%z, ( 0. N)%> + <%a, b%>) by A2, Def9;

        then <%y, ( 0. N)%> = <%z, ( 0. N)%> by A1;

        hence y = z by Th3;

      end;

      let y,z be Element of N such that

       A3: (y + b) = (z + b);

      ( <%( 0. N), y%> + <%a, b%>) = <%(( 0. N) + a), (y + b)%> by Def9

      .= ( <%( 0. N), z%> + <%a, b%>) by A3, Def9;

      then <%( 0. N), y%> = <%( 0. N), z%> by A1;

      hence y = z by Th3;

    end;

    theorem :: CAYLDICK:24

    a is add-cancelable & b is add-cancelable implies <%a, b%> is add-cancelable by Th20, Th22;

    theorem :: CAYLDICK:25

     <%a, b%> is add-cancelable implies a is add-cancelable & b is add-cancelable by Th21, Th23;

    theorem :: CAYLDICK:26

     <%a, b%> is left_complementable right_add-cancelable implies ( - <%a, b%>) = <%( - a), ( - b)%>

    proof

      assume

       A1: <%a, b%> is left_complementable right_add-cancelable;

      then a is left_complementable & b is left_complementable & a is right_add-cancelable & b is right_add-cancelable by Th15, Th23;

      then

       A2: (( - a) + a) = ( 0. N) & (( - b) + b) = ( 0. N) by ALGSTR_0:def 13;

      ( <%( - a), ( - b)%> + <%a, b%>) = <%(( - a) + a), (( - b) + b)%> by Def9

      .= ( 0. ( Cayley-Dickson N)) by A2, Def9;

      hence thesis by A1, ALGSTR_0:def 13;

    end;

    registration

      let N be add-associative non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> add-associative;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        set f = the addF of C;

        let a,b,c be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        consider a2,b2 be Element of N such that

         A2: b = <%a2, b2%> by Th12;

        consider a3,b3 be Element of N such that

         A3: c = <%a3, b3%> by Th12;

        

         A4: ((a1 + a2) + a3) = (a1 + (a2 + a3)) & ((b1 + b2) + b3) = (b1 + (b2 + b3)) by RLVECT_1:def 3;

        

         A5: (f . (b,c)) = <%(a2 + a3), (b2 + b3)%> by A2, A3, Def9;

        (f . (a,b)) = <%(a1 + a2), (b1 + b2)%> by A1, A2, Def9;

        

        hence ((a + b) + c) = <%((a1 + a2) + a3), ((b1 + b2) + b3)%> by A3, Def9

        .= (a + (b + c)) by A1, A4, A5, Def9;

      end;

    end

    registration

      let N be right_zeroed non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> right_zeroed;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        

         A2: ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        (a1 + ( 0. N)) = a1 & (b1 + ( 0. N)) = b1 by RLVECT_1:def 4;

        hence thesis by A1, A2, Def9;

      end;

    end

    registration

      let N be left_zeroed non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> left_zeroed;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        

         A2: ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        (( 0. N) + a1) = a1 & (( 0. N) + b1) = b1 by ALGSTR_1:def 2;

        hence thesis by A1, A2, Def9;

      end;

    end

    registration

      let N be right_complementable non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> right_complementable;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        consider a2 be Element of N such that

         A2: (a1 + a2) = ( 0. N) by ALGSTR_0:def 11;

        consider b2 be Element of N such that

         A3: (b1 + b2) = ( 0. N) by ALGSTR_0:def 11;

        take <%a2, b2%>;

        ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        hence thesis by A1, A2, A3, Def9;

      end;

    end

    registration

      let N be left_complementable non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> left_complementable;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        consider a2 be Element of N such that

         A2: (a2 + a1) = ( 0. N) by ALGSTR_0:def 10;

        consider b2 be Element of N such that

         A3: (b2 + b1) = ( 0. N) by ALGSTR_0:def 10;

        take <%a2, b2%>;

        ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        hence thesis by A1, A2, A3, Def9;

      end;

    end

    registration

      let N be Abelian non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> Abelian;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a,b be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        consider a2,b2 be Element of N such that

         A2: b = <%a2, b2%> by Th12;

        (the addF of C . (a,b)) = <%(a1 + a2), (b1 + b2)%> by A1, A2, Def9;

        hence thesis by A1, A2, Def9;

      end;

    end

    theorem :: CAYLDICK:27

    

     Th27: N is add-associative right_zeroed right_complementable implies ( - <%a, b%>) = <%( - a), ( - b)%>

    proof

      assume

       A1: N is add-associative right_zeroed right_complementable;

      then

       A2: (a + ( - a)) = ( 0. N) & (b + ( - b)) = ( 0. N) by RLVECT_1:def 10;

      ( <%a, b%> + <%( - a), ( - b)%>) = <%(a + ( - a)), (b + ( - b))%> by Def9

      .= ( 0. ( Cayley-Dickson N)) by A2, Def9;

      hence thesis by A1, RLVECT_1:def 10;

    end;

    theorem :: CAYLDICK:28

    

     Th28: N is add-associative right_zeroed right_complementable implies ( <%a1, b1%> - <%a2, b2%>) = <%(a1 - a2), (b1 - b2)%>

    proof

      assume N is add-associative right_zeroed right_complementable;

      

      hence ( <%a1, b1%> - <%a2, b2%>) = ( <%a1, b1%> + <%( - a2), ( - b2)%>) by Th27

      .= <%(a1 - a2), (b1 - b2)%> by Def9;

    end;

    registration

      let N be well-unital add-associative right_zeroed right_complementable distributive Banach_Algebra-like_2 well-conjugated scalar-unital almost_right_cancelable non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> well-unital;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let a be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        

         A3: ( 1. C) = <%( 1. N), ( 0. N)%> by Def9;

        then

         A4: (a * ( 1. C)) = <%((a1 * ( 1. N)) - ((( 0. N) *' ) * b1)), ((( 0. N) * a1) + (b1 * (( 1. N) *' )))%> by A1, Def9;

        (( 1. C) * a) = <%((( 1. N) * a1) - ((b1 *' ) * ( 0. N))), ((b1 * ( 1. N)) + (( 0. N) * (a1 *' )))%> by A1, A3, Def9;

        hence thesis by A1, A4;

      end;

    end

    registration

      let N be non degenerated non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> non degenerated;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        ( 0. C) = <%( 0. N), ( 0. N)%> & ( 1. C) = <%( 1. N), ( 0. N)%> by Def9;

        hence ( 0. C) <> ( 1. C);

      end;

    end

    registration

      let N be add-conjugative add-associative right_zeroed right_complementable Abelian non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> add-conjugative;

      coherence

      proof

        let a,b be Element of ( Cayley-Dickson N);

        consider a1,a2 be Element of N such that

         A1: a = <%a1, a2%> by Th12;

        consider b1,b2 be Element of N such that

         A2: b = <%b1, b2%> by Th12;

        

         A3: ((a1 + b1) *' ) = ((a1 *' ) + (b1 *' )) by Def5;

        

         A4: (a *' ) = <%(a1 *' ), ( - a2)%> & (b *' ) = <%(b1 *' ), ( - b2)%> by A1, A2, Def9;

        

         A5: ( - (a2 + b2)) = (( - a2) - b2) by RLVECT_1: 30;

        (a + b) = <%(a1 + b1), (a2 + b2)%> by A1, A2, Def9;

        

        hence ((a + b) *' ) = <%((a1 + b1) *' ), ( - (a2 + b2))%> by Def9

        .= ((a *' ) + (b *' )) by A3, A4, A5, Def9;

      end;

    end

    registration

      let N be norm-conjugative reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> norm-conjugative;

      coherence

      proof

        let a be Element of ( Cayley-Dickson N);

        consider a1,a2 be Element of N such that

         A1: a = <%a1, a2%> by Th12;

        

         A2: ||.(a1 *' ).|| = ||.a1.|| by Def6;

        

         A3: ||.( - a2).|| = ||.a2.|| by NORMSP_1: 2;

        (a *' ) = <%(a1 *' ), ( - a2)%> by A1, Def9;

        

        hence ||.(a *' ).|| = ( sqrt (( ||.(a1 *' ).|| ^2 ) + ( ||.( - a2).|| ^2 ))) by Def9

        .= ||.a.|| by A1, A2, A3, Def9;

      end;

    end

    registration

      let N be scalar-conjugative add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> scalar-conjugative;

      coherence

      proof

        let r;

        let a be Element of ( Cayley-Dickson N);

        consider a1,a2 be Element of N such that

         A1: a = <%a1, a2%> by Th12;

        

         A2: (r * ( - a2)) = ( - (r * a2)) by RLVECT_1: 25;

        (r * a) = <%(r * a1), (r * a2)%> by A1, Def9;

        then

         A3: ((r * a) *' ) = <%((r * a1) *' ), ( - (r * a2))%> by Def9;

        

         A4: (r * (a1 *' )) = ((r * a1) *' ) by Def7;

        (a *' ) = <%(a1 *' ), ( - a2)%> by A1, Def9;

        hence ((r * a) *' ) = (r * (a *' )) by A2, A3, A4, Def9;

      end;

    end

    registration

      let N be distributive add-associative right_zeroed right_complementable Abelian non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> left-distributive;

      coherence

      proof

        let a,b,c be Element of ( Cayley-Dickson N);

        consider a1,a2 be Element of N such that

         A1: a = <%a1, a2%> by Th12;

        consider b1,b2 be Element of N such that

         A2: b = <%b1, b2%> by Th12;

        consider c1,c2 be Element of N such that

         A3: c = <%c1, c2%> by Th12;

        

         A4: (b + c) = <%(b1 + c1), (b2 + c2)%> by A2, A3, Def9;

        

         A5: (b * a) = <%((b1 * a1) - ((a2 *' ) * b2)), ((a2 * b1) + (b2 * (a1 *' )))%> by A1, A2, Def9;

        

         A6: (c * a) = <%((c1 * a1) - ((a2 *' ) * c2)), ((a2 * c1) + (c2 * (a1 *' )))%> by A1, A3, Def9;

        

         A7: ((b1 + c1) * a1) = ((b1 * a1) + (c1 * a1)) by VECTSP_1:def 3;

        

         A8: (a2 * (b1 + c1)) = ((a2 * b1) + (a2 * c1)) by VECTSP_1:def 2;

        ((a2 *' ) * (b2 + c2)) = (((a2 *' ) * b2) + ((a2 *' ) * c2)) by VECTSP_1:def 2;

        

        then

         A9: (((b1 + c1) * a1) - ((a2 *' ) * (b2 + c2))) = ((((b1 * a1) + (c1 * a1)) - ((a2 *' ) * b2)) - ((a2 *' ) * c2)) by A7, RLVECT_1: 27

        .= ((((b1 * a1) - ((a2 *' ) * b2)) + (c1 * a1)) - ((a2 *' ) * c2)) by RLVECT_1: 28

        .= (((b1 * a1) - ((a2 *' ) * b2)) + ((c1 * a1) - ((a2 *' ) * c2))) by RLVECT_1: 28;

        ((b2 + c2) * (a1 *' )) = ((b2 * (a1 *' )) + (c2 * (a1 *' ))) by VECTSP_1:def 3;

        

        then

         A10: ((a2 * (b1 + c1)) + ((b2 + c2) * (a1 *' ))) = ((((a2 * b1) + (a2 * c1)) + (b2 * (a1 *' ))) + (c2 * (a1 *' ))) by A8, RLVECT_1:def 3

        .= ((((a2 * b1) + (b2 * (a1 *' ))) + (a2 * c1)) + (c2 * (a1 *' ))) by RLVECT_1:def 3

        .= (((a2 * b1) + (b2 * (a1 *' ))) + ((a2 * c1) + (c2 * (a1 *' )))) by RLVECT_1:def 3;

        

        thus ((b + c) * a) = <%(((b1 + c1) * a1) - ((a2 *' ) * (b2 + c2))), ((a2 * (b1 + c1)) + ((b2 + c2) * (a1 *' )))%> by A1, A4, Def9

        .= ((b * a) + (c * a)) by A5, A6, A9, A10, Def9;

      end;

    end

    registration

      let N be distributive add-associative right_zeroed right_complementable add-conjugative Abelian non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> right-distributive;

      coherence

      proof

        let a,b,c be Element of ( Cayley-Dickson N);

        consider a1,a2 be Element of N such that

         A1: a = <%a1, a2%> by Th12;

        consider b1,b2 be Element of N such that

         A2: b = <%b1, b2%> by Th12;

        consider c1,c2 be Element of N such that

         A3: c = <%c1, c2%> by Th12;

        

         A4: (a1 * (b1 + c1)) = ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 2;

        

         A5: ((b2 + c2) * a1) = ((b2 * a1) + (c2 * a1)) by VECTSP_1:def 3;

        ((b2 + c2) *' ) = ((b2 *' ) + (c2 *' )) by Def5;

        then (((b2 + c2) *' ) * a2) = (((b2 *' ) * a2) + ((c2 *' ) * a2)) by VECTSP_1:def 3;

        

        then

         A6: ((a1 * (b1 + c1)) - (((b2 + c2) *' ) * a2)) = ((((a1 * b1) + (a1 * c1)) - ((b2 *' ) * a2)) - ((c2 *' ) * a2)) by A4, RLVECT_1: 27

        .= ((((a1 * b1) - ((b2 *' ) * a2)) + (a1 * c1)) - ((c2 *' ) * a2)) by RLVECT_1:def 3

        .= (((a1 * b1) - ((b2 *' ) * a2)) + ((a1 * c1) - ((c2 *' ) * a2))) by RLVECT_1:def 3;

        ((b1 + c1) *' ) = ((b1 *' ) + (c1 *' )) by Def5;

        then (a2 * ((b1 + c1) *' )) = ((a2 * (b1 *' )) + (a2 * (c1 *' ))) by VECTSP_1:def 2;

        

        then

         A7: (((b2 + c2) * a1) + (a2 * ((b1 + c1) *' ))) = ((((b2 * a1) + (c2 * a1)) + (a2 * (b1 *' ))) + (a2 * (c1 *' ))) by A5, RLVECT_1:def 3

        .= ((((b2 * a1) + (a2 * (b1 *' ))) + (c2 * a1)) + (a2 * (c1 *' ))) by RLVECT_1:def 3

        .= (((b2 * a1) + (a2 * (b1 *' ))) + ((c2 * a1) + (a2 * (c1 *' )))) by RLVECT_1:def 3;

        

         A8: (a * b) = <%((a1 * b1) - ((b2 *' ) * a2)), ((b2 * a1) + (a2 * (b1 *' )))%> by A1, A2, Def9;

        

         A9: (a * c) = <%((a1 * c1) - ((c2 *' ) * a2)), ((c2 * a1) + (a2 * (c1 *' )))%> by A1, A3, Def9;

        (b + c) = <%(b1 + c1), (b2 + c2)%> by A2, A3, Def9;

        

        hence (a * (b + c)) = <%((a1 * (b1 + c1)) - (((b2 + c2) *' ) * a2)), (((b2 + c2) * a1) + (a2 * ((b1 + c1) *' )))%> by A1, Def9

        .= ((a * b) + (a * c)) by A6, A7, A8, A9, Def9;

      end;

    end

    registration

      let N be reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> RealNormSpace-like;

      coherence

      proof

        let c1,c2 be Element of ( Cayley-Dickson N);

        let r;

        consider a1,b1 be Element of N such that

         A1: c1 = <%a1, b1%> by Th12;

        

         A2: (r * c1) = <%(r * a1), (r * b1)%> by A1, Def9;

        

         A3: ||.(r * a1).|| = ( |.r.| * ||.a1.||) & ||.(r * b1).|| = ( |.r.| * ||.b1.||) by NORMSP_1:def 1;

        

        thus ||.(r * c1).|| = ( sqrt (( ||.(r * a1).|| ^2 ) + ( ||.(r * b1).|| ^2 ))) by A2, Def9

        .= ( sqrt (( |.r.| ^2 ) * (( ||.a1.|| ^2 ) + ( ||.b1.|| ^2 )))) by A3

        .= ( |.r.| * ( sqrt (( ||.a1.|| ^2 ) + ( ||.b1.|| ^2 )))) by SQUARE_1: 54

        .= ( |.r.| * ||.c1.||) by A1, Def9;

        consider a2,b2 be Element of N such that

         A4: c2 = <%a2, b2%> by Th12;

        set A1 = ||.a1.||, A2 = ||.a2.||, B1 = ||.b1.||, B2 = ||.b2.||, C1 = ||.c1.||, C2 = ||.c2.||;

         ||.(a1 + a2).|| <= (A1 + A2) & ||.(b1 + b2).|| <= (B1 + B2) by NORMSP_1:def 1;

        then ( ||.(a1 + a2).|| ^2 ) <= ((A1 + A2) ^2 ) & ( ||.(b1 + b2).|| ^2 ) <= ((B1 + B2) ^2 ) by XREAL_1: 66;

        then

         A5: (( ||.(a1 + a2).|| ^2 ) + ( ||.(b1 + b2).|| ^2 )) <= (((A1 + A2) ^2 ) + ((B1 + B2) ^2 )) by XREAL_1: 7;

        (c1 + c2) = <%(a1 + a2), (b1 + b2)%> by A1, A4, Def9;

        then

         A6: ||.(c1 + c2).|| = ( sqrt (( ||.(a1 + a2).|| ^2 ) + ( ||.(b1 + b2).|| ^2 ))) by Def9;

        

         A7: C1 = ( sqrt ((A1 ^2 ) + (B1 ^2 ))) & C2 = ( sqrt ((A2 ^2 ) + (B2 ^2 ))) by A1, A4, Def9;

        then 0 <= C1 & 0 <= C2 by SQUARE_1:def 2;

        then

         A8: (C1 + C2) = ( sqrt ((C1 + C2) ^2 )) by SQUARE_1:def 2;

        (((A1 + A2) ^2 ) + ((B1 + B2) ^2 )) <= ((C1 + C2) ^2 ) by A7, Th1;

        then (( ||.(a1 + a2).|| ^2 ) + ( ||.(b1 + b2).|| ^2 )) <= ((C1 + C2) ^2 ) by A5, XXREAL_0: 2;

        hence thesis by A6, A8, SQUARE_1: 26;

      end;

    end

    registration

      let N be vector-distributive non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> vector-distributive;

      coherence

      proof

        let r;

        let c1,c2 be Element of ( Cayley-Dickson N);

        consider a1,b1 be Element of N such that

         A1: c1 = <%a1, b1%> by Th12;

        consider a2,b2 be Element of N such that

         A2: c2 = <%a2, b2%> by Th12;

        

         A3: (r * (a1 + a2)) = ((r * a1) + (r * a2)) & (r * (b1 + b2)) = ((r * b1) + (r * b2)) by RLVECT_1:def 5;

        

         A4: (r * <%a1, b1%>) = <%(r * a1), (r * b1)%> & (r * <%a2, b2%>) = <%(r * a2), (r * b2)%> by Def9;

        (c1 + c2) = <%(a1 + a2), (b1 + b2)%> by A1, A2, Def9;

        

        hence (r * (c1 + c2)) = <%(r * (a1 + a2)), (r * (b1 + b2))%> by Def9

        .= ((r * c1) + (r * c2)) by A1, A2, A3, A4, Def9;

      end;

    end

    registration

      let N be vector-associative Banach_Algebra-like_3 add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> vector-associative;

      coherence

      proof

        let c1,c2 be Element of ( Cayley-Dickson N);

        let r;

        consider a1,b1 be Element of N such that

         A1: c1 = <%a1, b1%> by Th12;

        consider a2,b2 be Element of N such that

         A2: c2 = <%a2, b2%> by Th12;

        

         A3: (c1 * c2) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> by A1, A2, Def9;

        

         A4: (r * (a1 * a2)) = ((r * a1) * a2) by FUNCSDOM:def 9;

        (r * ((b2 *' ) * b1)) = ((b2 *' ) * (r * b1)) by LOPBAN_2:def 11;

        then

         A5: (r * ((a1 * a2) - ((b2 *' ) * b1))) = (((r * a1) * a2) - ((b2 *' ) * (r * b1))) by A4, RLVECT_1: 34;

        

         A6: (r * (b2 * a1)) = (b2 * (r * a1)) by LOPBAN_2:def 11;

        (r * (b1 * (a2 *' ))) = ((r * b1) * (a2 *' )) by FUNCSDOM:def 9;

        then

         A7: (r * ((b2 * a1) + (b1 * (a2 *' )))) = ((b2 * (r * a1)) + ((r * b1) * (a2 *' ))) by A6, RLVECT_1:def 5;

        (r * c1) = <%(r * a1), (r * b1)%> by A1, Def9;

        

        hence ((r * c1) * c2) = <%(((r * a1) * a2) - ((b2 *' ) * (r * b1))), ((b2 * (r * a1)) + ((r * b1) * (a2 *' )))%> by A2, Def9

        .= (r * (c1 * c2)) by A3, A5, A7, Def9;

      end;

    end

    registration

      let N be scalar-distributive non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> scalar-distributive;

      coherence

      proof

        let r, s;

        let c be Element of ( Cayley-Dickson N);

        consider a,b be Element of N such that

         A1: c = <%a, b%> by Th12;

        

         A2: ((r + s) * a) = ((r * a) + (s * a)) & ((r + s) * b) = ((r * b) + (s * b)) by RLVECT_1:def 6;

        

         A3: (r * <%a, b%>) = <%(r * a), (r * b)%> & (s * <%a, b%>) = <%(s * a), (s * b)%> by Def9;

        

        thus ((r + s) * c) = <%((r + s) * a), ((r + s) * b)%> by A1, Def9

        .= ((r * c) + (s * c)) by A1, A2, A3, Def9;

      end;

    end

    registration

      let N be scalar-associative non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> scalar-associative;

      coherence

      proof

        let r, s;

        let c be Element of ( Cayley-Dickson N);

        consider a,b be Element of N such that

         A1: c = <%a, b%> by Th12;

        

         A2: ((r * s) * a) = (r * (s * a)) & ((r * s) * b) = (r * (s * b)) by RLVECT_1:def 7;

        

        thus ((r * s) * c) = <%((r * s) * a), ((r * s) * b)%> by A1, Def9

        .= (r * <%(s * a), (s * b)%>) by A2, Def9

        .= (r * (s * c)) by A1, Def9;

      end;

    end

    registration

      let N be scalar-unital non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> scalar-unital;

      coherence

      proof

        let c be Element of ( Cayley-Dickson N);

        consider a,b be Element of N such that

         A1: c = <%a, b%> by Th12;

        (1 * a) = a & (1 * b) = b by RLVECT_1:def 8;

        hence thesis by A1, Def9;

      end;

    end

    registration

      let N be reflexive Banach_Algebra-like_2 non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> Banach_Algebra-like_2;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        

         A1: ||.( 1. N).|| = 1 by LOPBAN_2:def 10;

        ( 1. C) = <%( 1. N), ( 0. N)%> by Def9;

        

        hence ||.( 1. C).|| = ( sqrt (( ||.( 1. N).|| ^2 ) + ( ||.( 0. N).|| ^2 ))) by Def9

        .= 1 by A1, SQUARE_1: 18;

      end;

    end

    registration

      let N be Banach_Algebra-like_3 add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive vector-associative scalar-conjugative non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> Banach_Algebra-like_3;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let r;

        let a,b be Element of C;

        consider a1,b1 be Element of N such that

         A1: a = <%a1, b1%> by Th12;

        consider a2,b2 be Element of N such that

         A2: b = <%a2, b2%> by Th12;

        

         A3: (r * b) = <%(r * a2), (r * b2)%> by A2, Def9;

        

         A4: (a * b) = <%((a1 * a2) - ((b2 *' ) * b1)), ((b2 * a1) + (b1 * (a2 *' )))%> by A1, A2, Def9;

        

         A5: (a * (r * b)) = <%((a1 * (r * a2)) - (((r * b2) *' ) * b1)), (((r * b2) * a1) + (b1 * ((r * a2) *' )))%> by A1, A3, Def9;

        (r * (b2 *' )) = ((r * b2) *' ) by Def7;

        then

         A6: (r * ((b2 *' ) * b1)) = (((r * b2) *' ) * b1) by FUNCSDOM:def 9;

        

         A7: (r * ((a1 * a2) - ((b2 *' ) * b1))) = ((r * (a1 * a2)) - (r * ((b2 *' ) * b1))) by RLVECT_1: 34

        .= ((a1 * (r * a2)) - (((r * b2) *' ) * b1)) by A6, LOPBAN_2:def 11;

        

         A8: ((r * b2) * a1) = (r * (b2 * a1)) by FUNCSDOM:def 9;

        (r * (a2 *' )) = ((r * a2) *' ) by Def7;

        then (b1 * ((r * a2) *' )) = (r * (b1 * (a2 *' ))) by LOPBAN_2:def 11;

        then (((r * b2) * a1) + (b1 * ((r * a2) *' ))) = (r * ((b2 * a1) + (b1 * (a2 *' )))) by A8, RLVECT_1:def 5;

        hence thesis by A4, A5, A7, Def9;

      end;

    end

    theorem :: CAYLDICK:29

    for N be almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive Abelian scalar-distributive scalar-associative scalar-unital vector-distributive vector-associative reflexive discerning RealNormSpace-like almost_right_cancelable well-conjugated add-conjugative Banach_Algebra-like_2 Banach_Algebra-like_3 non degenerated ConjNormAlgStr holds for a,b be Element of N st (a is non zero or b is non zero) & <%a, b%> is right_mult-cancelable left_invertible holds ( / <%a, b%>) = <%((1 / (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) * (a *' )), ((1 / (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) * ( - b))%>

    proof

      let N be almost_left_invertible associative add-associative right_zeroed right_complementable well-unital distributive Abelian scalar-distributive scalar-associative scalar-unital vector-distributive vector-associative reflexive discerning RealNormSpace-like almost_right_cancelable well-conjugated add-conjugative Banach_Algebra-like_2 Banach_Algebra-like_3 non degenerated ConjNormAlgStr;

      let a,b be Element of N such that

       A1: a is non zero or b is non zero and

       A2: <%a, b%> is right_mult-cancelable left_invertible;

      set C = ( Cayley-Dickson N);

      set m = (1 / (( ||.a.|| ^2 ) + ( ||.b.|| ^2 )));

      

       A3: ((b *' ) * ( - b)) = ( - ((b *' ) * b)) by VECTSP_1: 8;

      

       A4: ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) by Th9;

      

       A5: ((b *' ) * b) = (( ||.b.|| ^2 ) * ( 1. N)) by Th9;

      ((b *' ) * (m * ( - b))) = (m * ((b *' ) * ( - b))) by LOPBAN_2:def 11;

      

      then

       A6: (((m * (a *' )) * a) - ((b *' ) * (m * ( - b)))) = (((m * (a *' )) * a) - ( - (m * ((b *' ) * b)))) by A3, RLVECT_1: 25

      .= (((m * (a *' )) * a) + (m * ((b *' ) * b)))

      .= ((m * ((a *' ) * a)) + (m * ((b *' ) * b))) by FUNCSDOM:def 9

      .= (m * (((a *' ) * a) + ((b *' ) * b))) by RLVECT_1:def 5

      .= (m * ((( ||.a.|| ^2 ) + ( ||.b.|| ^2 )) * ( 1. N))) by A4, A5, RLVECT_1:def 6

      .= ((m * (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) * ( 1. N)) by RLVECT_1:def 7

      .= (1 * ( 1. N)) by A1, XCMPLX_1: 106

      .= ( 1. N) by RLVECT_1:def 8;

      ((m * ( - b)) * (a *' )) = (m * (( - b) * (a *' ))) by FUNCSDOM:def 9

      .= (( - b) * (m * (a *' ))) by LOPBAN_2:def 11

      .= ( - (b * (m * (a *' )))) by VECTSP_1: 9;

      then

       A7: ((b * (m * (a *' ))) + ((m * ( - b)) * (a *' ))) = ( 0. N) by RLVECT_1:def 10;

      ( <%(m * (a *' )), (m * ( - b))%> * <%a, b%>) = <%(((m * (a *' )) * a) - ((b *' ) * (m * ( - b)))), ((b * (m * (a *' ))) + ((m * ( - b)) * (a *' )))%> by Def9

      .= ( 1. C) by A6, A7, Def9;

      hence thesis by A2, ALGSTR_0:def 30;

    end;

    registration

      let N be add-associative right_zeroed right_complementable distributive scalar-distributive scalar-unital vector-distributive discerning reflexive well-conjugated non empty ConjNormAlgStr;

      cluster ( Cayley-Dickson N) -> well-conjugated;

      coherence

      proof

        set C = ( Cayley-Dickson N);

        let c be Element of C;

        consider a,b be Element of N such that

         A1: c = <%a, b%> by Th12;

        

         A2: ( 0. C) = <%( 0. N), ( 0. N)%> by Def9;

        

         A3: (c *' ) = <%(a *' ), ( - b)%> by A1, Def9;

        

         A4: ||.c.|| = ( sqrt (( ||.a.|| ^2 ) + ( ||.b.|| ^2 ))) by A1, Def9;

        per cases ;

          case c is non zero;

          

           A5: ( 1. C) = <%( 1. N), ( 0. N)%> by Def9;

          

           A6: ((a *' ) * a) = (( ||.a.|| ^2 ) * ( 1. N)) & ((b *' ) * b) = (( ||.b.|| ^2 ) * ( 1. N)) by Th9;

          

           A7: (((a *' ) * a) - ((b *' ) * ( - b))) = (((a *' ) * a) - ( - ((b *' ) * b))) by VECTSP_1: 8

          .= (((a *' ) * a) + ((b *' ) * b))

          .= ((( ||.a.|| ^2 ) + ( ||.b.|| ^2 )) * ( 1. N)) by A6, RLVECT_1:def 6

          .= (( ||.c.|| ^2 ) * ( 1. N)) by A4, SQUARE_1:def 2;

          (b + ( - b)) = ( 0. N) by RLVECT_1:def 10;

          

          then ((b * (a *' )) + (( - b) * (a *' ))) = (( 0. N) * (a *' )) by VECTSP_1:def 3

          .= (( ||.c.|| ^2 ) * ( 0. N));

          

          then ((c *' ) * c) = <%(( ||.c.|| ^2 ) * ( 1. N)), (( ||.c.|| ^2 ) * ( 0. N))%> by A1, A3, A7, Def9

          .= (( ||.c.|| ^2 ) * ( 1. C)) by A5, Def9;

          hence thesis;

        end;

          case c is zero;

          then c = ( 0. C);

          then

           A8: a = ( 0. N) & b = ( 0. N) by A1, A2, Th3;

           ||.(c *' ).|| = 0 by A3, A8;

          hence (c *' ) = ( 0. C) by NORMSP_0:def 5;

        end;

      end;

    end

    registration

      cluster ( Cayley-Dickson N_Real ) -> associative commutative;

      coherence

      proof

        thus ( Cayley-Dickson N_Real ) is associative

        proof

          let x,y,z be Element of ( Cayley-Dickson N_Real );

          consider x1,x2 be Element of N_Real such that

           A1: x = <%x1, x2%> by Th12;

          consider y1,y2 be Element of N_Real such that

           A2: y = <%y1, y2%> by Th12;

          consider z1,z2 be Element of N_Real such that

           A3: z = <%z1, z2%> by Th12;

          set a1 = ((x1 * y1) - ((y2 *' ) * x2)), b1 = ((x1 * y2) + ((y1 *' ) * x2)), a2 = ((y1 * z1) - ((z2 *' ) * y2)), b2 = ((y1 * z2) + ((z1 *' ) * y2));

          

           A4: (y * z) = <%((y1 * z1) - ((z2 *' ) * y2)), ((y1 * z2) + ((z1 *' ) * y2))%> by A2, A3, Def9;

          (x * y) = <%((x1 * y1) - ((y2 *' ) * x2)), ((x1 * y2) + ((y1 *' ) * x2))%> by A1, A2, Def9;

          

          hence ((x * y) * z) = <%((a1 * z1) - ((z2 *' ) * b1)), ((a1 * z2) + ((z1 *' ) * b1))%> by A3, Def9

          .= <%((x1 * a2) - ((b2 *' ) * x2)), ((x1 * b2) + ((a2 *' ) * x2))%>

          .= (x * (y * z)) by A1, A4, Def9;

        end;

        let x,y be Element of ( Cayley-Dickson N_Real );

        consider x1,x2 be Element of N_Real such that

         A5: x = <%x1, x2%> by Th12;

        consider y1,y2 be Element of N_Real such that

         A6: y = <%y1, y2%> by Th12;

        

        thus (x * y) = <%((x1 * y1) - ((y2 *' ) * x2)), ((x1 * y2) + ((y1 *' ) * x2))%> by A5, A6, Def9

        .= <%((y1 * x1) - ((x2 *' ) * y2)), ((y1 * x2) + ((x1 *' ) * y2))%>

        .= (y * x) by A5, A6, Def9;

      end;

    end

    set z = ( 0. N_Real ), j = ( 1. N_Real );

    set ZJ = <%z, j%>, ZZ = <%z, z%>, JZ = <%j, z%>, ZM = <%z, ( - j)%>, MZ = <%( - j), z%>;

    

     Lm2: (ZJ * JZ) = <%((z * j) - ((z *' ) * j)), ((z * z) + ((j *' ) * j))%> by Def9

    .= <%z, ((j *' ) * j)%>;

    theorem :: CAYLDICK:30

    

     Th30: ( <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%> * <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>) = <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 1. N_Real )%>%>

    proof

      

      thus <%ZZ, ZJ%> = <%((ZJ * ZZ) - ((JZ *' ) * ZZ)), ((ZJ * JZ) + ((ZZ *' ) * ZZ))%> by Lm2

      .= ( <%ZJ, ZZ%> * <%ZZ, JZ%>) by Def9;

    end;

    theorem :: CAYLDICK:31

    

     Th31: ( <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%> * <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>) = <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( - ( 1. N_Real ))%>%>

    proof

      (ZJ *' ) = <%(z *' ), ( - j)%> by Def9;

      then ((ZJ *' ) * JZ) = <%((z * j) - ((z *' ) * ( - j))), ((z * z) + ((j *' ) * ( - j)))%> by Def9;

      

      hence <%ZZ, ZM%> = <%((ZZ * ZJ) - ((ZZ *' ) * JZ)), ((ZZ * ZZ) + ((ZJ *' ) * JZ))%>

      .= ( <%ZZ, JZ%> * <%ZJ, ZZ%>) by Def9;

    end;

    registration

      cluster ( Cayley-Dickson ( Cayley-Dickson N_Real )) -> associative non commutative;

      coherence

      proof

        thus ( Cayley-Dickson ( Cayley-Dickson N_Real )) is associative

        proof

          let a,b,c be Element of ( Cayley-Dickson ( Cayley-Dickson N_Real ));

          consider a1,b1,a2,b2 be Element of N_Real such that

           A1: a = <% <%a1, b1%>, <%a2, b2%>%> by Th13;

          consider a3,b3,a4,b4 be Element of N_Real such that

           A2: b = <% <%a3, b3%>, <%a4, b4%>%> by Th13;

          consider a5,b5,a6,b6 be Element of N_Real such that

           A3: c = <% <%a5, b5%>, <%a6, b6%>%> by Th13;

          set x1 = (( <%a1, b1%> * <%a3, b3%>) - (( <%a4, b4%> *' ) * <%a2, b2%>));

          set x2 = (( <%a1, b1%> * <%a4, b4%>) + (( <%a3, b3%> *' ) * <%a2, b2%>));

          set x3 = (( <%a3, b3%> * <%a5, b5%>) - (( <%a6, b6%> *' ) * <%a4, b4%>));

          set x4 = (( <%a3, b3%> * <%a6, b6%>) + (( <%a5, b5%> *' ) * <%a4, b4%>));

          set x11 = (((a1 * a3) - ((b3 *' ) * b1)) - (((a4 *' ) * a2) - ((b2 *' ) * ( - b4))));

          set x12 = (((a1 * b3) + ((a3 *' ) * b1)) - (((a4 *' ) * b2) + ((a2 *' ) * ( - b4))));

          set x21 = (((a1 * a4) - ((b4 *' ) * b1)) + (((a3 *' ) * a2) - ((b2 *' ) * ( - b3))));

          set x22 = (((a1 * b4) + ((a4 *' ) * b1)) + (((a3 *' ) * b2) + ((a2 *' ) * ( - b3))));

          set x31 = (((a3 * a5) - ((b5 *' ) * b3)) - (((a6 *' ) * a4) - ((b4 *' ) * ( - b6))));

          set x32 = (((a3 * b5) + ((a5 *' ) * b3)) - (((a6 *' ) * b4) + ((a4 *' ) * ( - b6))));

          set x41 = (((a3 * a6) - ((b6 *' ) * b3)) + (((a5 *' ) * a4) - ((b4 *' ) * ( - b5))));

          set x42 = (((a3 * b6) + ((a6 *' ) * b3)) + (((a5 *' ) * b4) + ((a4 *' ) * ( - b5))));

          

           A4: ( <%a1, b1%> * <%a3, b3%>) = <%((a1 * a3) - ((b3 *' ) * b1)), ((a1 * b3) + ((a3 *' ) * b1))%> by Def9;

          

           A5: ( <%a4, b4%> *' ) = <%(a4 *' ), ( - b4)%> by Def9;

          

           A6: ( <%(a4 *' ), ( - b4)%> * <%a2, b2%>) = <%(((a4 *' ) * a2) - ((b2 *' ) * ( - b4))), (((a4 *' ) * b2) + ((a2 *' ) * ( - b4)))%> by Def9;

          

           A7: x1 = <%x11, x12%> by A4, A5, A6, Th28;

          

           A8: ( <%a1, b1%> * <%a4, b4%>) = <%((a1 * a4) - ((b4 *' ) * b1)), ((a1 * b4) + ((a4 *' ) * b1))%> by Def9;

          

           A9: ( <%a3, b3%> *' ) = <%(a3 *' ), ( - b3)%> by Def9;

          

           A10: ( <%(a3 *' ), ( - b3)%> * <%a2, b2%>) = <%(((a3 *' ) * a2) - ((b2 *' ) * ( - b3))), (((a3 *' ) * b2) + ((a2 *' ) * ( - b3)))%> by Def9;

          

           A11: x2 = <%x21, x22%> by A8, A9, A10, Def9;

          

           A12: ( <%a3, b3%> * <%a5, b5%>) = <%((a3 * a5) - ((b5 *' ) * b3)), ((a3 * b5) + ((a5 *' ) * b3))%> by Def9;

          

           A13: ( <%a6, b6%> *' ) = <%(a6 *' ), ( - b6)%> by Def9;

          

           A14: ( <%(a6 *' ), ( - b6)%> * <%a4, b4%>) = <%(((a6 *' ) * a4) - ((b4 *' ) * ( - b6))), (((a6 *' ) * b4) + ((a4 *' ) * ( - b6)))%> by Def9;

          

           A15: x3 = <%x31, x32%> by A12, A13, A14, Th28;

          

           A16: ( <%a3, b3%> * <%a6, b6%>) = <%((a3 * a6) - ((b6 *' ) * b3)), ((a3 * b6) + ((a6 *' ) * b3))%> by Def9;

          

           A17: ( <%a5, b5%> *' ) = <%(a5 *' ), ( - b5)%> by Def9;

          

           A18: ( <%(a5 *' ), ( - b5)%> * <%a4, b4%>) = <%(((a5 *' ) * a4) - ((b4 *' ) * ( - b5))), (((a5 *' ) * b4) + ((a4 *' ) * ( - b5)))%> by Def9;

          

           A19: x4 = <%x41, x42%> by A16, A17, A18, Def9;

          

           A20: ( <%a1, b1%> * x3) = <%((a1 * x31) - ((x32 *' ) * b1)), ((a1 * x32) + ((x31 *' ) * b1))%> by A15, Def9;

          (x4 *' ) = <%(x41 *' ), ( - x42)%> by A19, Def9;

          then

           A21: ((x4 *' ) * <%a2, b2%>) = <%(((x41 *' ) * a2) - ((b2 *' ) * ( - x42))), (((x41 *' ) * b2) + ((a2 *' ) * ( - x42)))%> by Def9;

          

           A22: (x1 * <%a5, b5%>) = <%((x11 * a5) - ((b5 *' ) * x12)), ((x11 * b5) + ((a5 *' ) * x12))%> by A7, Def9;

          (( <%a6, b6%> *' ) * x2) = <%(((a6 *' ) * x21) - ((x22 *' ) * ( - b6))), (((a6 *' ) * x22) + ((x21 *' ) * ( - b6)))%> by A11, A13, Def9;

          

          then

           A23: ((x1 * <%a5, b5%>) - (( <%a6, b6%> *' ) * x2)) = <%(((x11 * a5) - ((b5 *' ) * x12)) - (((a6 *' ) * x21) - ((x22 *' ) * ( - b6)))), (((x11 * b5) + ((a5 *' ) * x12)) - (((a6 *' ) * x22) + ((x21 *' ) * ( - b6))))%> by A22, Th28

          .= <%(((a1 * x31) - ((x32 *' ) * b1)) - (((x41 *' ) * a2) - ((b2 *' ) * ( - x42)))), (((a1 * x32) + ((x31 *' ) * b1)) - (((x41 *' ) * b2) + ((a2 *' ) * ( - x42))))%>

          .= (( <%a1, b1%> * x3) - ((x4 *' ) * <%a2, b2%>)) by A20, A21, Th28;

          

           A24: ( <%a1, b1%> * x4) = <%((a1 * x41) - ((x42 *' ) * b1)), ((a1 * x42) + ((x41 *' ) * b1))%> by A19, Def9;

          (x3 *' ) = <%(x31 *' ), ( - x32)%> by A15, Def9;

          then

           A25: ((x3 *' ) * <%a2, b2%>) = <%(((x31 *' ) * a2) - ((b2 *' ) * ( - x32))), (((x31 *' ) * b2) + ((a2 *' ) * ( - x32)))%> by Def9;

          

           A26: (x1 * <%a6, b6%>) = <%((x11 * a6) - ((b6 *' ) * x12)), ((x11 * b6) + ((a6 *' ) * x12))%> by A7, Def9;

          (( <%a5, b5%> *' ) * x2) = <%(((a5 *' ) * x21) - ((x22 *' ) * ( - b5))), (((a5 *' ) * x22) + ((x21 *' ) * ( - b5)))%> by A17, A11, Def9;

          

          then

           A27: ((x1 * <%a6, b6%>) + (( <%a5, b5%> *' ) * x2)) = <%(((x11 * a6) - ((b6 *' ) * x12)) + (((a5 *' ) * x21) - ((x22 *' ) * ( - b5)))), (((x11 * b6) + ((a6 *' ) * x12)) + (((a5 *' ) * x22) + ((x21 *' ) * ( - b5))))%> by A26, Def9

          .= <%(((a1 * x41) - ((x42 *' ) * b1)) + (((x31 *' ) * a2) - ((b2 *' ) * ( - x32)))), (((a1 * x42) + ((x41 *' ) * b1)) + (((x31 *' ) * b2) + ((a2 *' ) * ( - x32))))%>

          .= (( <%a1, b1%> * x4) + ((x3 *' ) * <%a2, b2%>)) by A24, A25, Def9;

          

           A28: (b * c) = <%x3, x4%> by A2, A3, Def9;

          (a * b) = <%x1, x2%> by A1, A2, Def9;

          

          hence ((a * b) * c) = <%((x1 * <%a5, b5%>) - (( <%a6, b6%> *' ) * x2)), ((x1 * <%a6, b6%>) + (( <%a5, b5%> *' ) * x2))%> by A3, Def9

          .= (a * (b * c)) by A1, A28, A23, A27, Def9;

        end;

        take <%ZJ, ZZ%>, <%ZZ, JZ%>;

        ZJ <> ZM by Th3;

        hence thesis by Th30, Th31, Th3;

      end;

    end

    set ZZZZ = <%ZZ, ZZ%>, JZZZ = <%JZ, ZZ%>, ZJZZ = <%ZJ, ZZ%>, ZZJZ = <%ZZ, JZ%>, ZZZJ = <%ZZ, ZJ%>;

    

     Lm3: (ZJ *' ) = <%(z *' ), ( - j)%> by Def9;

    theorem :: CAYLDICK:32

    

     Th32: ( <% <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%> * <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>) = <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 1. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>

    proof

      

       A1: ((ZJZZ * ZZJZ) - ((ZZZZ *' ) * ZZZZ)) = <%((ZJ * ZZ) - ((JZ *' ) * ZZ)), ((ZJ * JZ) + ((ZZ *' ) * ZZ))%> by Def9

      .= <%ZZ, (ZJ * JZ)%>

      .= ZZZJ by Lm2;

      ((ZZZZ * ZJZZ) + (ZZZZ * (ZZJZ *' ))) = ZZZZ;

      hence thesis by A1, Def9;

    end;

    theorem :: CAYLDICK:33

    

     Th33: ( <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%> * <% <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>) = <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( - ( 1. N_Real ))%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>

    proof

      

       A1: (JZ * (ZJ *' )) = <%((j * (z *' )) - ((( - j) *' ) * z)), ((( - j) * j) + (z * ((z *' ) *' )))%> by Lm3, Def9

      .= <%z, ( - j)%>;

      

       A2: ((ZZJZ * ZJZZ) - ((ZZZZ *' ) * ZZZZ)) = <%((ZZ * ZJ) - ((ZZ *' ) * JZ)), ((ZZ * ZZ) + (JZ * (ZJ *' )))%> by Def9

      .= <%ZZ, ZM%> by A1;

      ((ZZZZ * ZZJZ) + (ZZZZ * (ZJZZ *' ))) = ZZZZ;

      hence ( <%ZZJZ, ZZZZ%> * <%ZJZZ, ZZZZ%>) = <% <%ZZ, ZM%>, ZZZZ%> by A2, Def9;

    end;

    theorem :: CAYLDICK:34

    

     Th34: (( <% <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%> * <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>) * <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>) = <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( - ( 1. N_Real )), ( 0. N_Real )%>%>%>

    proof

      set a1 = ((ZJZZ * ZZJZ) - ((ZZZZ *' ) * ZZZZ)), b1 = ((ZZZZ * ZJZZ) + (ZZZZ * (ZZJZ *' )));

      

       A1: (ZJ * ZJ) = <%((z * z) - ((j *' ) * j)), ((z * j) + ((z *' ) * j))%> by Def9

      .= <%( - j), z%>;

      a1 = <%((ZJ * ZZ) - ((JZ *' ) * ZZ)), ((ZJ * JZ) + ((ZZ *' ) * ZZ))%> by Def9

      .= <%ZZ, (ZJ * JZ)%>

      .= ZZZJ by Lm2;

      

      then

       A2: (ZJZZ * a1) = <%((ZJ * ZZ) - ((ZJ *' ) * ZZ)), ((ZJ * ZJ) + (ZZ * (ZZ *' )))%> by Def9

      .= <%ZZ, (ZJ * ZJ)%>;

      ( <%ZJZZ, ZZZZ%> * <%ZZJZ, ZZZZ%>) = <%a1, b1%> by Def9;

      

      hence (( <%ZJZZ, ZZZZ%> * <%ZZJZ, ZZZZ%>) * <%ZZZZ, ZJZZ%>) = <%((a1 * ZZZZ) - ((ZJZZ *' ) * b1)), ((ZJZZ * a1) + (b1 * (ZZZZ *' )))%> by Def9

      .= <%ZZZZ, (ZJZZ * a1)%>

      .= <%ZZZZ, <%ZZ, MZ%>%> by A1, A2;

    end;

    theorem :: CAYLDICK:35

    

     Th35: ( <% <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%> * ( <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%> * <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 1. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>%>)) = <% <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 0. N_Real ), ( 0. N_Real )%>%>, <% <%( 0. N_Real ), ( 0. N_Real )%>, <%( 1. N_Real ), ( 0. N_Real )%>%>%>

    proof

      set a1 = ((ZZJZ * ZZZZ) - ((ZJZZ *' ) * ZZZZ)), b1 = ((ZJZZ * ZZJZ) + (ZZZZ * (ZZZZ *' )));

      

       A1: (ZJ * (ZJ *' )) = <%((z * z) - ((( - j) *' ) * j)), ((( - j) * z) + (j * (z *' )))%> by Lm3, Def9;

      

       A2: (JZ * ZJ) = <%((j * z) - ((j *' ) * z)), ((j * j) + (z * (z *' )))%> by Def9;

      b1 = <%((ZJ * ZZ) - ((JZ *' ) * ZZ)), ((JZ * ZJ) + (ZZ * (ZZ *' )))%> by Def9

      .= <%ZZ, (JZ * ZJ)%>;

      

      then

       A3: (b1 * ZJZZ) = <%((ZZ * ZJ) - ((ZZ *' ) * ZJ)), ((ZZ * ZZ) + (ZJ * (ZJ *' )))%> by A2, Def9

      .= <%ZZ, JZ%> by A1;

      ( <%ZZJZ, ZZZZ%> * <%ZZZZ, ZJZZ%>) = <%a1, b1%> by Def9;

      

      hence ( <%ZJZZ, ZZZZ%> * ( <%ZZJZ, ZZZZ%> * <%ZZZZ, ZJZZ%>)) = <%((ZJZZ * a1) - ((b1 *' ) * ZZZZ)), ((b1 * ZJZZ) + (ZZZZ * (a1 *' )))%> by Def9

      .= <%ZZZZ, (b1 * ZJZZ)%>

      .= <%ZZZZ, ZZJZ%> by A3;

    end;

    registration

      cluster ( Cayley-Dickson ( Cayley-Dickson ( Cayley-Dickson N_Real ))) -> non associative non commutative;

      coherence

      proof

        thus ( Cayley-Dickson ( Cayley-Dickson ( Cayley-Dickson N_Real ))) is non associative

        proof

          take <%ZJZZ, ZZZZ%>, <%ZZJZ, ZZZZ%>, <%ZZZZ, ZJZZ%>;

           <%( - j), z%> <> JZ by Th3;

          then <%ZZ, <%( - j), z%>%> <> ZZJZ by Th3;

          hence thesis by Th34, Th35, Th3;

        end;

        take <%ZJZZ, ZZZZ%>, <%ZZJZ, ZZZZ%>;

        ZJ <> <%z, ( - j)%> by Th3;

        then <%ZZ, <%z, ( - j)%>%> <> ZZZJ by Th3;

        hence thesis by Th32, Th33, Th3;

      end;

    end