matrtop3.miz



    begin

    reserve x,X for set,

r,r1,r2,s for Real,

i,j,k,m,n for Nat;

    theorem :: MATRTOP3:1

    

     Th1: for K be Field, M be Matrix of n, K holds for P be Permutation of ( Seg n) holds ( Det ((((M * P) @ ) * P) @ )) = ( Det M) & for i, j st [i, j] in ( Indices M) holds (((((M * P) @ ) * P) @ ) * (i,j)) = (M * ((P . i),(P . j)))

    proof

      let K be Field, M be Matrix of n, K;

      let P be Permutation of ( Seg n);

      reconsider p = P as Element of ( Permutations n) by MATRIX_1:def 12;

      

       A1: ( - ( - ( Det M))) = ( Det M) by RLVECT_1: 17;

      

       A2: p is even & ( - (( Det M),p)) = ( Det M) or p is odd & ( - (( Det M),p)) = ( - ( Det M)) by MATRIX_1:def 16;

      

      thus ( Det ((((M * P) @ ) * P) @ )) = ( Det (((M * P) @ ) * P)) by MATRIXR2: 43

      .= ( - (( Det ((M * P) @ )),p)) by MATRIX11: 46

      .= ( - (( Det (M * P)),p)) by MATRIXR2: 43

      .= ( - (( - (( Det M),p)),p)) by MATRIX11: 46

      .= ( Det M) by A1, A2, MATRIX_1:def 16;

      let i, j;

      assume

       A3: [i, j] in ( Indices M);

      ( Indices M) = ( Indices ((((M * P) @ ) * P) @ )) by MATRIX_0: 26;

      then

       A4: [j, i] in ( Indices (((M * P) @ ) * P)) by A3, MATRIX_0:def 6;

      then

       A5: (((((M * P) @ ) * P) @ ) * (i,j)) = ((((M * P) @ ) * P) * (j,i)) by MATRIX_0:def 6;

      ( Indices M) = ( Indices (((M * P) @ ) * P)) & ( Indices M) = ( Indices ((M * P) @ )) by MATRIX_0: 26;

      then

       A6: ex k st k = (P . j) & [k, i] in ( Indices ((M * P) @ )) & ((((M * P) @ ) * P) * (j,i)) = (((M * P) @ ) * (k,i)) by A4, MATRIX11: 37;

      then

       A7: [i, (P . j)] in ( Indices (M * P)) by MATRIX_0:def 6;

      ( Indices (M * P)) = ( Indices M) by MATRIX_0: 26;

      then ((M * P) * (i,(P . j))) = (M * ((P . i),(P . j))) by A7, MATRIX11:def 4;

      hence (((((M * P) @ ) * P) @ ) * (i,j)) = (M * ((P . i),(P . j))) by A5, A6, A7, MATRIX_0:def 6;

    end;

    theorem :: MATRTOP3:2

    

     Th2: for K be Field holds for M be diagonal Matrix of n, K holds (M @ ) = M

    proof

      let K be Field;

      let M be diagonal Matrix of n, K;

      for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((M @ ) * (i,j))

      proof

        let i, j;

        assume

         A1: [i, j] in ( Indices M);

        then

         A2: [j, i] in ( Indices M) by MATRIX_0: 28;

        then

         A3: ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

        per cases ;

          suppose i = j;

          hence thesis by A1, MATRIX_0:def 6;

        end;

          suppose

           A4: i <> j;

          then (M * (i,j)) = ( 0. K) by A1, MATRIX_1:def 6;

          hence thesis by A2, A3, A4, MATRIX_1:def 6;

        end;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: MATRTOP3:3

    

     Th3: for f be real-valued FinSequence holds for i st i in ( dom f) holds ( Sum ( sqr (f +* (i,r)))) = ((( Sum ( sqr f)) - ((f . i) ^2 )) + (r ^2 ))

    proof

      let f be real-valued FinSequence;

      let i such that

       A1: i in ( dom f);

      reconsider fi = (f . i) as Element of REAL by XREAL_0:def 1;

      set F = ( @ ( @ f));

      set G = (F | (i -' 1)), H = (F /^ i);

      

       A2: ( sqr <*fi*>) = <*(fi ^2 )*> by RVSUM_1: 55;

      F = (F +* (i,fi)) by FUNCT_7: 35

      .= ((G ^ <*fi*>) ^ H) by A1, FUNCT_7: 98;

      

      then ( sqr F) = (( sqr (G ^ <*fi*>)) ^ ( sqr H)) by RVSUM_1: 144

      .= ((( sqr G) ^ ( sqr <*fi*>)) ^ ( sqr H)) by RVSUM_1: 144;

      

      then

       A3: ( Sum ( sqr F)) = (( Sum (( sqr G) ^ ( sqr <*fi*>))) + ( Sum ( sqr H))) by RVSUM_1: 75

      .= ((( Sum ( sqr G)) + (fi ^2 )) + ( Sum ( sqr H))) by A2, RVSUM_1: 74;

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

      

       A4: ( sqr <*R*>) = <*(R ^2 )*> by RVSUM_1: 55;

      (F +* (i,R)) = ((G ^ <*R*>) ^ H) by A1, FUNCT_7: 98;

      

      then ( sqr (F +* (i,R))) = (( sqr (G ^ <*R*>)) ^ ( sqr H)) by RVSUM_1: 144

      .= ((( sqr G) ^ ( sqr <*R*>)) ^ ( sqr H)) by RVSUM_1: 144;

      

      then ( Sum ( sqr (F +* (i,R)))) = (( Sum (( sqr G) ^ ( sqr <*R*>))) + ( Sum ( sqr H))) by RVSUM_1: 75

      .= ((( Sum ( sqr G)) + (R ^2 )) + ( Sum ( sqr H))) by A4, RVSUM_1: 74;

      hence thesis by A3;

    end;

    definition

      let X;

      let F be Function-yielding Function;

      :: MATRTOP3:def1

      attr F is X -support-yielding means

      : Def1: for f be Function, x st f in ( dom F) & ((F . f) . x) <> (f . x) holds x in X;

    end

    registration

      let X;

      cluster X -support-yielding for Function-yielding Function;

      existence

      proof

        reconsider F = {} as Function-yielding Function;

        F is X -support-yielding;

        hence thesis;

      end;

    end

    registration

      let X;

      let Y be Subset of X;

      cluster Y -support-yielding -> X -support-yielding for Function-yielding Function;

      coherence

      proof

        let F be Function-yielding Function;

        assume

         A1: F is Y -support-yielding;

        let f be Function, x be set;

        assume f in ( dom F) & ((F . f) . x) <> (f . x);

        then x in Y by A1;

        hence thesis;

      end;

    end

    registration

      let X,Y be set;

      cluster X -support-yieldingY -support-yielding -> (X /\ Y) -support-yielding for Function-yielding Function;

      coherence

      proof

        let F be Function-yielding Function;

        assume

         A1: F is X -support-yieldingY -support-yielding;

        let f be Function, x be set;

        assume f in ( dom F) & ((F . f) . x) <> (f . x);

        then x in X & x in Y by A1;

        hence thesis by XBOOLE_0:def 4;

      end;

      let f be X -support-yielding Function-yielding Function;

      let g be Y -support-yielding Function-yielding Function;

      cluster (f * g) -> (X \/ Y) -support-yielding;

      coherence

      proof

        set fg = (f * g);

        let h be Function, x be set;

        assume that

         A2: h in ( dom fg) and

         A3: ((fg . h) . x) <> (h . x);

        

         A4: h in ( dom g) by A2, FUNCT_1: 11;

        assume

         A5: not x in (X \/ Y);

        then not x in Y by XBOOLE_0:def 3;

        then

         A6: ((g . h) . x) = (h . x) by A4, Def1;

        

         A7: (fg . h) = (f . (g . h)) & (g . h) in ( dom f) by A2, FUNCT_1: 11, FUNCT_1: 12;

         not x in X by A5, XBOOLE_0:def 3;

        hence thesis by A3, A6, A7, Def1;

      end;

    end

    registration

      let n;

      cluster homogeneous for Function of ( TOP-REAL n), ( TOP-REAL n);

      existence

      proof

        reconsider N = n as Element of NAT by ORDINAL1:def 12;

         the homogeneous Function of ( TOP-REAL N), ( TOP-REAL N) is homogeneous;

        hence thesis;

      end;

    end

    registration

      let n, m;

      cluster -> FinSequence-yielding for Function of ( TOP-REAL n), ( TOP-REAL m);

      coherence

      proof

        let F be Function of ( TOP-REAL n), ( TOP-REAL m);

        now

          let x be object;

          assume x in ( dom F);

          then ( rng F) c= the carrier of ( TOP-REAL m) & (F . x) in ( rng F) by FUNCT_1:def 3, RELAT_1:def 19;

          hence (F . x) is FinSequence;

        end;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    registration

      let n, m;

      let A be Matrix of n, m, F_Real ;

      cluster ( Mx2Tran A) -> additive;

      coherence by MATRTOP1: 22;

    end

    registration

      let n;

      let A be Matrix of n, F_Real ;

      cluster ( Mx2Tran A) -> homogeneous;

      coherence by MATRTOP1: 23;

    end

    registration

      let n;

      let f,g be homogeneous Function of ( TOP-REAL n), ( TOP-REAL n);

      cluster (f * g) -> homogeneous;

      coherence

      proof

        set TR = ( TOP-REAL n);

        now

          let r be Real, p be Point of TR;

          reconsider gp = (g . p) as Point of TR;

          

           A1: ( dom (f * g)) = the carrier of TR by FUNCT_2: 52;

          

          hence ((f * g) . (r * p)) = (f . (g . (r * p))) by FUNCT_1: 12

          .= (f . (r * gp)) by TOPREAL9:def 4

          .= (r * (f . gp)) by TOPREAL9:def 4

          .= (r * ((f * g) . p)) by A1, FUNCT_1: 12;

        end;

        hence thesis;

      end;

    end

    begin

    reserve p,q for Point of ( TOP-REAL n);

    

     Lm1: i in ( Seg n) implies ex M be Matrix of n, F_Real st ( Det M) = ( - ( 1. F_Real )) & (M * (i,i)) = ( - ( 1. F_Real )) & for k, m st [k, m] in ( Indices M) holds (k = m & k <> i implies (M * (k,k)) = ( 1. F_Real )) & (k <> m implies (M * (k,m)) = ( 0. F_Real ))

    proof

      set FR = the carrier of F_Real ;

      set mm = the multF of F_Real ;

      reconsider N = n as Element of NAT by ORDINAL1:def 12;

      defpred P[ set, set, set] means ($1 = $2 & $1 = i implies $3 = ( - ( 1. F_Real ))) & ($1 = $2 & $1 <> i implies $3 = ( 1. F_Real )) & ($1 <> $2 implies $3 = ( 0. F_Real ));

      

       A1: for k, m st [k, m] in [:( Seg N), ( Seg N):] holds ex x be Element of F_Real st P[k, m, x]

      proof

        let k, m;

        assume [k, m] in [:( Seg N), ( Seg N):];

        k = m & k = i or k = m & k <> i or k <> m;

        hence thesis;

      end;

      consider M be Matrix of N, F_Real such that

       A2: for n, m st [n, m] in ( Indices M) holds P[n, m, (M * (n,m))] from MATRIX_0:sch 2( A1);

      reconsider M as Matrix of n, F_Real ;

      

       A3: ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      now

        let k,m be Nat;

        assume k in ( Seg n) & m in ( Seg n);

        then

         A4: [k, m] in ( Indices M) by A3, ZFMISC_1: 87;

        assume k <> m;

        hence (M * (k,m)) = ( 0. F_Real ) by A2, A4;

      end;

      then

       A5: M is diagonal by MATRIX_7:def 2;

      set D = ( diagonal_of_Matrix M);

      defpred R[ Nat] means ($1 + i) <= n implies (mm "**" (D | ($1 + i))) = ( - ( 1. F_Real ));

      

       A6: ( len D) = n by MATRIX_3:def 10;

      

       A7: for k st R[k] holds R[(k + 1)]

      proof

        let k;

        assume

         A8: R[k];

        set k1 = (k + 1), ki = (k1 + i);

        assume

         A9: (k1 + i) <= n;

        

         A10: (k1 + i) = ((k + i) + 1);

        then

         A11: 1 <= ki by NAT_1: 11;

        then ki in ( dom D) by A6, A9, FINSEQ_3: 25;

        then

         A12: (D | ki) = ((D | (k + i)) ^ <*(D . ki)*>) by A10, FINSEQ_5: 10;

        i <= (k + i) by NAT_1: 11;

        then

         A13: i < (k1 + i) by A10, NAT_1: 13;

        

         A14: ki in ( Seg n) by A9, A11;

        then [ki, ki] in ( Indices M) by A3, ZFMISC_1: 87;

        

        then ( 1. F_Real ) = (M * (ki,ki)) by A2, A13

        .= (D . ki) by A14, MATRIX_3:def 10;

        

        hence (mm "**" (D | ki)) = (( - ( 1. F_Real )) * ( 1. F_Real )) by A8, A9, A10, A12, FINSOP_1: 4, NAT_1: 13

        .= (( - ( 1. F_Real )) * 1)

        .= ( - ( 1. F_Real ));

      end;

      defpred P[ Nat] means $1 < i implies (mm "**" (D | $1)) = ( 1. F_Real );

      

       A15: P[ 0 ]

      proof

        assume 0 < i;

        (D | 0 ) = ( <*> the carrier of F_Real ) & ( the_unity_wrt mm) = ( 1. F_Real ) by FVSUM_1: 5;

        hence thesis by FINSOP_1: 10;

      end;

      assume

       A16: i in ( Seg n);

      then

       A17: 1 <= i by FINSEQ_1: 1;

      

       A18: i <= n by A16, FINSEQ_1: 1;

      then

       A19: ((n - i) + i) = n & (n - i) is Nat by NAT_1: 21;

      take M;

      

       A20: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A21: P[k];

        set k1 = (k + 1);

        assume

         A22: k1 < i;

        then

         A23: 1 <= k1 & k1 <= n by A18, NAT_1: 14, XXREAL_0: 2;

        then k1 in ( dom D) by A6, FINSEQ_3: 25;

        then

         A24: (D | k1) = ((D | k) ^ <*(D . k1)*>) by FINSEQ_5: 10;

        

         A25: k1 in ( Seg n) by A23;

        then [k1, k1] in ( Indices M) by A3, ZFMISC_1: 87;

        

        then ( 1. F_Real ) = (M * (k1,k1)) by A2, A22

        .= (D . k1) by A25, MATRIX_3:def 10;

        

        hence (mm "**" (D | k1)) = (( 1. F_Real ) * ( 1. F_Real )) by A21, A22, A24, FINSOP_1: 4, NAT_1: 13

        .= (( 1. F_Real ) * 1)

        .= ( 1. F_Real );

      end;

      

       A26: for k holds P[k] from NAT_1:sch 2( A15, A20);

      

       A27: R[ 0 ]

      proof

        reconsider I = (i - 1) as Nat by A17;

        assume ( 0 + i) <= n;

        

         A28: (I + 1) = i;

        then I < i by NAT_1: 13;

        then

         A29: (mm "**" (D | I)) = ( 1. F_Real ) by A26;

        1 <= i by A16, FINSEQ_1: 1;

        then i in ( dom D) by A6, A18, FINSEQ_3: 25;

        then

         A30: (D | i) = ((D | I) ^ <*(D . i)*>) by A28, FINSEQ_5: 10;

         [i, i] in ( Indices M) by A3, A16, ZFMISC_1: 87;

        

        then ( - ( 1. F_Real )) = (M * (i,i)) by A2

        .= (D . i) by A16, MATRIX_3:def 10;

        

        hence (mm "**" (D | ( 0 + i))) = (( 1. F_Real ) * ( - ( 1. F_Real ))) by A29, A30, FINSOP_1: 4

        .= (1 * ( - ( 1. F_Real )))

        .= ( - ( 1. F_Real ));

      end;

      for k holds R[k] from NAT_1:sch 2( A27, A7);

      

      hence ( - ( 1. F_Real )) = (mm "**" (D | n)) by A19

      .= (mm "**" D) by A6, FINSEQ_1: 58

      .= ( Det M) by A5, A17, A18, MATRIX_7: 17, XXREAL_0: 2;

       [i, i] in ( Indices M) by A3, A16, ZFMISC_1: 87;

      hence (M * (i,i)) = ( - ( 1. F_Real )) by A2;

      let k, m;

      assume [k, m] in ( Indices M);

      hence thesis by A2;

    end;

    definition

      let n, i;

      :: MATRTOP3:def2

      func AxialSymmetry (i,n) -> invertible Matrix of n, F_Real means

      : Def2: (it * (i,i)) = ( - ( 1. F_Real )) & for k, m st [k, m] in ( Indices it ) holds (k = m & k <> i implies (it * (k,k)) = ( 1. F_Real )) & (k <> m implies (it * (k,m)) = ( 0. F_Real ));

      existence

      proof

        consider M be Matrix of n, F_Real such that

         A2: ( Det M) = ( - ( 1. F_Real )) and

         A3: (M * (i,i)) = ( - ( 1. F_Real )) & for k, m st [k, m] in ( Indices M) holds (k = m & k <> i implies (M * (k,k)) = ( 1. F_Real )) & (k <> m implies (M * (k,m)) = ( 0. F_Real )) by A1, Lm1;

        ( Det M) <> ( 0. F_Real ) by A2;

        then M is invertible by LAPLACE: 34;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let A1,A2 be invertible Matrix of n, F_Real such that

         A4: (A1 * (i,i)) = ( - ( 1. F_Real )) and

         A5: for k, m st [k, m] in ( Indices A1) holds (k = m & k <> i implies (A1 * (k,k)) = ( 1. F_Real )) & (k <> m implies (A1 * (k,m)) = ( 0. F_Real )) and

         A6: (A2 * (i,i)) = ( - ( 1. F_Real )) and

         A7: for k, m st [k, m] in ( Indices A2) holds (k = m & k <> i implies (A2 * (k,k)) = ( 1. F_Real )) & (k <> m implies (A2 * (k,m)) = ( 0. F_Real ));

        for k, m st [k, m] in ( Indices A1) holds (A1 * (k,m)) = (A2 * (k,m))

        proof

          let k, m;

          assume

           A8: [k, m] in ( Indices A1);

          then

           A9: [k, m] in ( Indices A2) by MATRIX_0: 26;

          per cases ;

            suppose

             A10: k <> m;

            then (A1 * (k,m)) = ( 0. F_Real ) by A5, A8;

            hence thesis by A7, A9, A10;

          end;

            suppose

             A11: k = m & k <> i;

            then (A1 * (k,m)) = ( 1. F_Real ) by A5, A8;

            hence thesis by A7, A9, A11;

          end;

            suppose k = m & k = i;

            hence thesis by A4, A6;

          end;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: MATRTOP3:4

    

     Th4: i in ( Seg n) implies ( Det ( AxialSymmetry (i,n))) = ( - ( 1. F_Real ))

    proof

      assume

       A1: i in ( Seg n);

      then

      consider M be Matrix of n, F_Real such that

       A2: ( Det M) = ( - ( 1. F_Real )) and

       A3: (M * (i,i)) = ( - ( 1. F_Real )) & for k, m st [k, m] in ( Indices M) holds (k = m & k <> i implies (M * (k,k)) = ( 1. F_Real )) & (k <> m implies (M * (k,m)) = ( 0. F_Real )) by Lm1;

      ( Det M) <> ( 0. F_Real ) by A2;

      then M is invertible by LAPLACE: 34;

      hence thesis by A1, A2, A3, Def2;

    end;

    theorem :: MATRTOP3:5

    

     Th5: i in ( Seg n) & j in ( Seg n) & i <> j implies (( @ p) "*" ( Col (( AxialSymmetry (i,n)),j))) = (p . j)

    proof

      set S = ( Seg n);

      assume that

       A1: i in S and

       A2: j in S and

       A3: i <> j;

      set A = ( AxialSymmetry (i,n)), C = ( Col (A,j));

      

       A4: ( Indices A) = [:S, S:] by MATRIX_0: 24;

      then

       A5: [j, j] in ( Indices A) by A2, ZFMISC_1: 87;

      

       A6: ( len A) = n by MATRIX_0: 25;

      then

       A7: ( dom A) = S by FINSEQ_1:def 3;

      ( len C) = n by A6, MATRIX_0:def 8;

      then

       A8: ( dom C) = S by FINSEQ_1:def 3;

       A9:

      now

        let m such that

         A10: m in ( dom C) and

         A11: m <> j;

        

         A12: [m, j] in ( Indices A) by A2, A4, A8, A10, ZFMISC_1: 87;

        

        thus (C . m) = (A * (m,j)) by A7, A8, A10, MATRIX_0:def 8

        .= ( 0. F_Real ) by A1, A11, A12, Def2;

      end;

      ( len p) = n by CARD_1:def 7;

      then

       A13: ( dom p) = S by FINSEQ_1:def 3;

      (C . j) = (A * (j,j)) by A2, A7, MATRIX_0:def 8

      .= ( 1. F_Real ) by A1, A3, A5, Def2;

      

      hence (p . j) = ( Sum ( mlt (C,( @ p)))) by A2, A8, A9, A13, MATRIX_3: 17

      .= (( @ p) "*" C) by FVSUM_1: 64;

    end;

    theorem :: MATRTOP3:6

    

     Th6: i in ( Seg n) implies (( @ p) "*" ( Col (( AxialSymmetry (i,n)),i))) = ( - (p . i))

    proof

      set S = ( Seg n);

      assume

       A1: i in S;

      reconsider pI = (( @ p) . i) as Element of F_Real by XREAL_0:def 1;

      set A = ( AxialSymmetry (i,n)), C = ( Col (A,i));

      

       A2: ( len A) = n by MATRIX_0: 25;

      then

       A3: ( dom A) = S by FINSEQ_1:def 3;

      then

       A4: (C . i) = (A * (i,i)) by A1, MATRIX_0:def 8;

      ( len p) = n & ( len C) = n by A2, CARD_1:def 7;

      then ( len ( mlt (( @ p),C))) = n by MATRIX_3: 6;

      then

       A5: ( dom ( mlt (( @ p),C))) = S by FINSEQ_1:def 3;

      

       A6: ( Indices A) = [:S, S:] by MATRIX_0: 24;

      

       A7: for k st k in ( dom ( mlt (( @ p),C))) & k <> i holds (( mlt (( @ p),C)) . k) = ( 0. F_Real )

      proof

        let k;

        assume that

         A8: k in ( dom ( mlt (( @ p),C))) and

         A9: k <> i;

        (( @ p) . k) in REAL by XREAL_0:def 1;

        then

        reconsider pk = (( @ p) . k) as Element of F_Real ;

        

         A10: [k, i] in ( Indices A) by A1, A5, A6, A8, ZFMISC_1: 87;

        (C . k) = (A * (k,i)) by A3, A5, A8, MATRIX_0:def 8;

        

        hence (( mlt (( @ p),C)) . k) = (pk * (A * (k,i))) by A8, FVSUM_1: 60

        .= (pk * ( 0. F_Real )) by A1, A9, A10, Def2

        .= ( 0. F_Real );

      end;

      

      thus (( @ p) "*" C) = (( mlt (( @ p),C)) . i) by A1, A5, A7, MATRIX_3: 12

      .= (pI * (A * (i,i))) by A1, A4, A5, FVSUM_1: 60

      .= (pI * ( - ( 1. F_Real ))) by A1, Def2

      .= (pI * ( - 1))

      .= ( - (p . i));

    end;

    theorem :: MATRTOP3:7

    

     Th7: i in ( Seg n) implies ( AxialSymmetry (i,n)) is diagonal & (( AxialSymmetry (i,n)) ~ ) = ( AxialSymmetry (i,n))

    proof

      set S = ( Seg n), A = ( AxialSymmetry (i,n));

      set ONE = ( 1. ( F_Real ,n)), AA = (A * A);

      assume

       A1: i in S;

      for k, m st [k, m] in ( Indices A) & (A * (k,m)) <> ( 0. F_Real ) holds k = m by A1, Def2;

      hence A is diagonal by MATRIX_1:def 6;

      for k, m st [k, m] in ( Indices AA) holds (AA * (k,m)) = (ONE * (k,m))

      proof

        let k, m such that

         A2: [k, m] in ( Indices AA);

        

         A3: ( width A) = n by MATRIX_0: 24;

        then ( len ( @ ( Line (A,k)))) = n by CARD_1:def 7;

        then

        reconsider L = ( @ ( Line (A,k))) as Element of ( TOP-REAL n) by TOPREAL3: 46;

        ( len A) = n by MATRIX_0: 25;

        then

         A4: (AA * (k,m)) = (( @ L) "*" ( Col (A,m))) by A2, A3, MATRIX_3:def 4;

        

         A5: ( Indices AA) = [:S, S:] by MATRIX_0: 24;

        then

         A6: m in S by A2, ZFMISC_1: 87;

        then

         A7: (( Line (A,k)) . m) = (A * (k,m)) by A3, MATRIX_0:def 7;

        

         A8: ( Indices A) = [:S, S:] by MATRIX_0: 24;

        

         A9: ( Indices ONE) = [:S, S:] by MATRIX_0: 24;

        per cases ;

          suppose

           A10: m <> i;

          then

           A11: (AA * (k,m)) = (A * (k,m)) by A1, A4, A6, A7, Th5;

          per cases ;

            suppose

             A12: k <> m;

            then (ONE * (k,m)) = ( 0. F_Real ) by A2, A5, A9, MATRIX_1:def 3;

            hence thesis by A1, A2, A5, A8, A11, A12, Def2;

          end;

            suppose

             A13: k = m;

            then (ONE * (k,m)) = ( 1. F_Real ) by A2, A5, A9, MATRIX_1:def 3;

            hence thesis by A1, A2, A5, A8, A10, A11, A13, Def2;

          end;

        end;

          suppose

           A14: m = i;

          then

           A15: (AA * (k,m)) = ( - (A * (k,m))) by A4, A6, A7, Th6;

          per cases ;

            suppose

             A16: k <> m;

            then (A * (k,m)) = ( 0. F_Real ) by A1, A2, A5, A8, Def2;

            hence thesis by A2, A5, A9, A15, A16, MATRIX_1:def 3;

          end;

            suppose

             A17: k = m;

            then (AA * (k,m)) = ( - ( - ( 1. F_Real ))) by A1, A14, A15, Def2;

            hence thesis by A2, A5, A9, A17, MATRIX_1:def 3;

          end;

        end;

      end;

      then AA = ONE by MATRIX_0: 27;

      then A is_reverse_of A by MATRIX_6:def 2;

      hence thesis by MATRIX_6:def 4;

    end;

    theorem :: MATRTOP3:8

    

     Th8: i in ( Seg n) & i <> j implies ((( Mx2Tran ( AxialSymmetry (i,n))) . p) . j) = (p . j)

    proof

      set A = ( AxialSymmetry (i,n)), M = ( Mx2Tran A), Mp = (M . p), S = ( Seg n);

      assume

       A1: i in S & i <> j;

      ( len Mp) = n by CARD_1:def 7;

      then

       A2: ( dom Mp) = S by FINSEQ_1:def 3;

      ( len p) = n by CARD_1:def 7;

      then

       A3: ( dom p) = S by FINSEQ_1:def 3;

      per cases ;

        suppose

         A4: j in S;

        then 1 <= j & j <= n by FINSEQ_1: 1;

        

        hence (Mp . j) = (( @ p) "*" ( Col (A,j))) by MATRTOP1: 18

        .= (p . j) by A1, A4, Th5;

      end;

        suppose

         A5: not j in S;

        then (Mp . j) = {} by A2, FUNCT_1:def 2;

        hence thesis by A3, A5, FUNCT_1:def 2;

      end;

    end;

    theorem :: MATRTOP3:9

    

     Th9: i in ( Seg n) implies ((( Mx2Tran ( AxialSymmetry (i,n))) . p) . i) = ( - (p . i))

    proof

      set A = ( AxialSymmetry (i,n)), M = ( Mx2Tran A), Mp = (M . p), S = ( Seg n);

      assume

       A1: i in S;

      then 1 <= i & i <= n by FINSEQ_1: 1;

      

      hence (Mp . i) = (( @ p) "*" ( Col (A,i))) by MATRTOP1: 18

      .= ( - (p . i)) by A1, Th6;

    end;

    theorem :: MATRTOP3:10

    

     Th10: i in ( Seg n) implies (( Mx2Tran ( AxialSymmetry (i,n))) . p) = (p +* (i,( - (p . i))))

    proof

      set S = ( Seg n), Mp = (( Mx2Tran ( AxialSymmetry (i,n))) . p), p0 = (p +* (i,( - (p . i))));

      

       A1: ( len p) = n by CARD_1:def 7;

      assume

       A2: i in S;

      

       A3: for j st 1 <= j & j <= n holds (Mp . j) = (p0 . j)

      proof

        let j such that

         A4: 1 <= j & j <= n;

        

         A5: j in S by A4;

        

         A6: j in ( dom p) by A1, A4, FINSEQ_3: 25;

        per cases ;

          suppose

           A7: j <> i;

          then (p0 . j) = (p . j) by FUNCT_7: 32;

          hence thesis by A2, A7, Th8;

        end;

          suppose

           A8: j = i;

          then (p0 . j) = ( - (p . i)) by A6, FUNCT_7: 31;

          hence thesis by A5, A8, Th9;

        end;

      end;

      ( len p0) = ( len p) & ( len Mp) = n by CARD_1:def 7, FUNCT_7: 97;

      hence thesis by A1, A3;

    end;

    theorem :: MATRTOP3:11

    

     Th11: i in ( Seg n) implies ( Mx2Tran ( AxialSymmetry (i,n))) is {i} -support-yielding

    proof

      set M = ( Mx2Tran ( AxialSymmetry (i,n)));

      assume

       A1: i in ( Seg n);

      let f be Function, x be set;

      assume f in ( dom M);

      then

      reconsider F = f as Point of ( TOP-REAL n) by FUNCT_2: 52;

      assume

       A2: ((M . f) . x) <> (f . x);

      ( len (M . F)) = n by CARD_1:def 7;

      then

       A3: ( dom (M . F)) = ( Seg n) by FINSEQ_1:def 3;

      

       A4: ( len F) = n by CARD_1:def 7;

      then

       A5: ( dom F) = ( Seg n) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A6: not x in ( Seg n);

        

        then ((M . F) . x) = {} by A3, FUNCT_1:def 2

        .= (F . x) by A5, A6, FUNCT_1:def 2;

        hence thesis by A2;

      end;

        suppose x in ( Seg n);

        then x = i by A1, A2, A4, Th8;

        hence thesis by TARSKI:def 1;

      end;

    end;

    theorem :: MATRTOP3:12

    

     Th12: for a,b be Element of F_Real st a = ( cos r) & b = ( sin r) holds ( Det ( block_diagonal ( <*((a,b) ][ (( - b),a)), ( 1. ( F_Real ,n))*>,( 0. F_Real )))) = ( 1. F_Real )

    proof

      let a,b be Element of F_Real ;

      set A = ((a,b) ][ (( - b),a));

      set ONE = ( 1. ( F_Real ,n));

      set B = ( block_diagonal ( <*A, ONE*>,( 0. F_Real )));

      

       A1: n = 0 or n >= 1 by NAT_1: 14;

      

       A2: ( Det ONE) = ( 1_ F_Real ) or ( Det ONE) = ( 1. F_Real ) by A1, MATRIXR2: 41, MATRIX_7: 16;

      assume a = ( cos r) & b = ( sin r);

      

      then

       A3: ((( cos r) * ( cos r)) + (( sin r) * ( sin r))) = ((a * a) - (b * ( - b)))

      .= ( Det A) by MATRIX_9: 13;

      

       A4: ( cos r) = ( cos . r) & ( sin r) = ( sin . r) by SIN_COS:def 17, SIN_COS:def 19;

      

      thus ( Det B) = (( Det A) * ( Det ONE)) by MATRIXJ1: 52

      .= ( 1. F_Real ) by A2, A3, A4, SIN_COS: 28;

    end;

    

     Lm2: 1 <= i & i < j & j <= n implies ex P be Permutation of ( Seg n) st (P . 1) = i & (P . 2) = j & for k st k in ( Seg n) & k > 2 holds (k <= (i + 1) implies (P . k) = (k - 2)) & ((i + 1) < k & k <= j implies (P . k) = (k - 1)) & (k > j implies (P . k) = k)

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= n;

      i <= n by A2, A3, XXREAL_0: 2;

      then

       A4: i in ( Seg n) by A1;

      1 <= j by A1, A2, XXREAL_0: 2;

      then

       A5: j in ( Seg n) by A3;

      reconsider S = ( Seg n) as non empty Subset of NAT by A1, A2, A3;

      defpred P[ Nat, Nat] means ($1 = 1 implies $2 = i) & ($1 = 2 implies $2 = j) & ($1 > 2 implies ($1 <= (i + 1) implies $2 = ($1 - 2)) & ((i + 1) < $1 & $1 <= j implies $2 = ($1 - 1)) & ($1 > j implies $2 = $1));

      

       A6: (i + 1) < (j + 1) by A2, XREAL_1: 8;

      

       A7: for k st k in ( Seg n) holds ex d be Element of S st P[k, d]

      proof

        let k;

        assume

         A8: k in ( Seg n);

        then

         A9: k <= n by FINSEQ_1: 1;

        

         A10: k <> 0 by A8;

        k <= 2 implies k = 0 or ... or k = 2;

        per cases by A10;

          suppose k = 1 or k = 2;

          hence thesis by A4, A5;

        end;

          suppose

           A11: k > 2 & k <> 1 & k <> 2;

          then

          reconsider k2 = (k - 2) as Nat by NAT_1: 21;

          k2 > (2 - 2) by A11, XREAL_1: 8;

          then

           A12: k2 >= 1 by NAT_1: 14;

          

           A13: k2 <= (k - 0 ) by XREAL_1: 10;

          per cases by A8;

            suppose

             A14: k <= (i + 1);

            then k < (j + 1) by A6, XXREAL_0: 2;

            then

             A15: k <= j by NAT_1: 13;

            k2 <= n by A9, A13, XXREAL_0: 2;

            then k2 in S by A12;

            hence thesis by A11, A14, A15;

          end;

            suppose

             A16: k > (i + 1) & k <= j;

            set k1 = (k2 + 1);

            k1 <= (k1 + 1) by NAT_1: 11;

            then

             A17: k1 <= n by A9, XXREAL_0: 2;

            k1 >= 1 by NAT_1: 11;

            then k1 in S by A17;

            hence thesis by A11, A16;

          end;

            suppose k > (i + 1) & k > j & k in S;

            hence thesis by A11;

          end;

        end;

      end;

      consider f be FinSequence of S such that

       A18: ( len f) = n & for k st k in ( Seg n) holds P[k, (f /. k)] from FINSEQ_4:sch 1( A7);

      

       A19: 1 < j by A1, A2, XXREAL_0: 2;

      then 1 <= n by A3, XXREAL_0: 2;

      then

       A20: 1 in S;

      then

       A21: P[1, (f /. 1)] by A18;

      (1 + 1) <= j by A19, NAT_1: 13;

      then 2 <= n by A3, XXREAL_0: 2;

      then

       A22: 2 in S;

      then

       A23: P[2, (f /. 2)] by A18;

      

       A24: ( dom f) = S by A18, FINSEQ_1:def 3;

      then

       A25: (f /. 1) = (f . 1) by A20, PARTFUN1:def 6;

      

       A26: ( rng f) c= S by FINSEQ_1:def 4;

      then

      reconsider F = f as Function of S, S by A24, FUNCT_2: 2;

      

       A27: (f /. 2) = (f . 2) by A22, A24, PARTFUN1:def 6;

      S c= ( rng f)

      proof

        let x be object;

        assume

         A28: x in S;

        then

        reconsider k = x as Nat;

        set k1 = (k + 1), k2 = (k1 + 1);

        

         A29: 1 <= k by A28, FINSEQ_1: 1;

        per cases by XXREAL_0: 1;

          suppose

           A30: k < i;

          

           A31: (k + 2) > ( 0 qua Nat + 2) by A29, XREAL_1: 8;

          

           A32: k1 <= i by A30, NAT_1: 13;

          then k1 < j by A2, XXREAL_0: 2;

          then k2 <= j by NAT_1: 13;

          then 1 <= k2 & k2 <= n by A3, NAT_1: 11, XXREAL_0: 2;

          then

           A33: k2 in S;

          then P[k2, (f /. k2)] by A18;

          then (f . k2) = k by A24, A31, A32, A33, PARTFUN1:def 6, XREAL_1: 6;

          hence thesis by A24, A33, FUNCT_1:def 3;

        end;

          suppose k = i;

          hence thesis by A20, A21, A24, A25, FUNCT_1:def 3;

        end;

          suppose

           A34: k > i & k < j;

          then k > 1 by A1, A29, XXREAL_0: 1;

          then

           A35: k >= (1 + 1) by NAT_1: 13;

          k1 <= j by A34, NAT_1: 13;

          then 1 <= k1 & k1 <= n by A3, NAT_1: 11, XXREAL_0: 2;

          then

           A36: k1 in S;

          then P[k1, (f /. k1)] by A18;

          then (f . k1) = k by A24, A34, A35, A36, NAT_1: 13, PARTFUN1:def 6, XREAL_1: 8;

          hence thesis by A24, A36, FUNCT_1:def 3;

        end;

          suppose k = j;

          hence thesis by A22, A23, A24, A27, FUNCT_1:def 3;

        end;

          suppose

           A37: k > j;

          j > 1 by A1, A2, XXREAL_0: 2;

          then

           A38: j >= (1 + 1) by NAT_1: 13;

           P[k, (f /. k)] by A18, A28;

          then (f . k) = k by A24, A37, A38, PARTFUN1:def 6, XXREAL_0: 2;

          hence thesis by A24, A28, FUNCT_1:def 3;

        end;

      end;

      then ( rng F) = S by A26, XBOOLE_0:def 10;

      then

       A39: F is onto by FUNCT_2:def 3;

      ( card S) = ( card S);

      then F is one-to-one by A39, FINSEQ_4: 63;

      then

      reconsider F as Permutation of ( Seg n) by A39;

      take F;

      thus (F . 1) = i & (F . 2) = j by A20, A21, A22, A23, A24, PARTFUN1:def 6;

      let k such that

       A40: k in ( Seg n) and

       A41: k > 2;

      (f /. k) = (f . k) by A24, A40, PARTFUN1:def 6;

      hence thesis by A18, A40, A41;

    end;

    

     Lm3: 1 <= i & i < j & j <= n implies ex A be Matrix of n, F_Real st ( Det A) = ( 1. F_Real ) & (A * (i,i)) = ( cos r) & (A * (j,j)) = ( cos r) & (A * (i,j)) = ( sin r) & (A * (j,i)) = ( - ( sin r)) & for k, m st [k, m] in ( Indices A) holds (k = m & k <> i & k <> j implies (A * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (A * (k,m)) = ( 0. F_Real ))

    proof

       A1:

      now

        let k;

        assume that

         A2: k >= 1 & k <> 1 and

         A3: k <> 2;

        k > 1 by A2, XXREAL_0: 1;

        then k >= (1 + 1) by NAT_1: 13;

        hence k > 2 by A3, XXREAL_0: 1;

      end;

      reconsider s = ( sin r), c = ( cos r) as Element of F_Real by XREAL_0:def 1;

      set S = ( Seg n);

      assume that

       A4: 1 <= i and

       A5: i < j and

       A6: j <= n;

      

       A7: 1 < j by A4, A5, XXREAL_0: 2;

      then

       A8: (1 + 1) <= j by NAT_1: 13;

      then

      reconsider n2 = (n - 2) as Nat by A6, NAT_1: 21, XXREAL_0: 2;

      consider P be Permutation of S such that

       A9: (P . 1) = i and

       A10: (P . 2) = j and for k st k in ( Seg n) & k > 2 holds (k <= (i + 1) implies (P . k) = (k - 2)) & ((i + 1) < k & k <= j implies (P . k) = (k - 1)) & (k > j implies (P . k) = k) by A4, A5, A6, Lm2;

      reconsider p = P as one-to-one Function;

      ( dom P) = S by FUNCT_2: 52;

      then

       A11: ( rng (p " )) = S by FUNCT_1: 33;

      ( rng P) = S by FUNCT_2:def 3;

      then ( dom (p " )) = S by FUNCT_1: 33;

      then

      reconsider P1 = (p " ) as one-to-one Function of S, S by A11, FUNCT_2: 1;

      P1 is onto by A11, FUNCT_2:def 3;

      then

      reconsider P1 as Permutation of S;

      

       A12: ( dom P) = S by FUNCT_2: 52;

      1 <= n by A6, A7, XXREAL_0: 2;

      then

       A13: 1 in S;

      then

       A14: (P1 . (P . 1)) = 1 by A12, FUNCT_1: 34;

      set A = ((c,s) ][ (( - s),c)), ONE = ( 1. ( F_Real ,n2)), ao = <*A, ONE*>;

      set B = ( block_diagonal (ao,( 0. F_Real )));

      

       A15: ( len A) = 2 by MATRIX_0: 25;

      then ( Len <*A*>) = <*2*> by MATRIXJ1: 15;

      then

       A16: ( Sum ( Len <*A*>)) = 2 by RVSUM_1: 73;

      ( len ONE) = n2 by MATRIX_0: 25;

      then

       A17: ( Sum ( Len ao)) = (2 + n2) by A15, MATRIXJ1: 16;

      then

      reconsider B as Matrix of n, F_Real ;

      

       A18: ( Indices B) = [:S, S:] by MATRIX_0: 24;

      2 <= n by A6, A8, XXREAL_0: 2;

      then

       A19: 2 in S;

      then

       A20: (P1 . (P . 2)) = 2 by A12, FUNCT_1: 34;

      set pBp = ((((B * P1) @ ) * P1) @ );

      

       A21: ( dom P1) = S by FUNCT_2: 52;

      i < n by A5, A6, XXREAL_0: 2;

      then

       A22: i in S by A4;

      then [i, i] in ( Indices B) by A18, ZFMISC_1: 87;

      then

       A23: (pBp * (i,i)) = (B * (1,1)) by A9, A14, Th1;

      take pBp;

      

       A24: ( Indices pBp) = [:S, S:] by MATRIX_0: 24;

      

       A25: ( Det B) = ( 1. F_Real ) by A17, Th12;

      

       A26: ( block_diagonal ( <*A*>,( 0. F_Real ))) = A by MATRIXJ1: 34;

      ( width A) = 2 by MATRIX_0: 24;

      then ( Width <*A*>) = <*2*> by MATRIXJ1: 19;

      then

       A27: ( Sum ( Width <*A*>)) = 2 by RVSUM_1: 73;

      1 < j by A4, A5, XXREAL_0: 2;

      then

       A28: j in S by A6;

      then [j, j] in ( Indices B) by A18, ZFMISC_1: 87;

      then

       A29: (pBp * (j,j)) = (B * (2,2)) by A10, A20, Th1;

      

       A30: ( block_diagonal ( <*ONE*>,( 0. F_Real ))) = ONE by MATRIXJ1: 34;

       [1, 1] in ( Indices A) by MATRIX_0: 48;

      then

       A31: (B * (1,1)) = (A * (1,1)) by A26, A30, MATRIXJ1: 26;

       [2, 1] in ( Indices A) by MATRIX_0: 48;

      then

       A32: (B * (2,1)) = (A * (2,1)) by A26, A30, MATRIXJ1: 26;

       [1, 2] in ( Indices A) by MATRIX_0: 48;

      then

       A33: (B * (1,2)) = (A * (1,2)) by A26, A30, MATRIXJ1: 26;

       [2, 2] in ( Indices A) by MATRIX_0: 48;

      then

       A34: (B * (2,2)) = (A * (2,2)) by A26, A30, MATRIXJ1: 26;

      

       A35: ( <*A*> ^ <*ONE*>) = ao;

       [i, j] in ( Indices B) by A18, A22, A28, ZFMISC_1: 87;

      then

       A36: (pBp * (i,j)) = (B * (1,2)) by A9, A10, A14, A20, Th1;

       [j, i] in ( Indices B) by A18, A22, A28, ZFMISC_1: 87;

      then (pBp * (j,i)) = (B * (2,1)) by A9, A10, A14, A20, Th1;

      hence ( Det pBp) = ( 1. F_Real ) & (pBp * (i,i)) = ( cos r) & (pBp * (j,j)) = ( cos r) & (pBp * (i,j)) = ( sin r) & (pBp * (j,i)) = ( - ( sin r)) by A23, A25, A29, A34, A33, A32, A31, A36, Th1, MATRIX_0: 50;

      let k, m such that

       A37: [k, m] in ( Indices pBp);

      

       A38: k in S by A24, A37, ZFMISC_1: 87;

      set Pk = (P1 . k), Pm = (P1 . m);

      

       A39: ( rng P1) = S by FUNCT_2:def 3;

      then

       A40: Pk in S by A21, A38, FUNCT_1:def 3;

      then

       A41: Pk >= 1 by FINSEQ_1: 1;

      

       A42: m in S by A24, A37, ZFMISC_1: 87;

      then

       A43: Pm in S by A21, A39, FUNCT_1:def 3;

      then

       A44: [Pk, Pm] in [:S, S:] by A40, ZFMISC_1: 87;

      

       A45: (pBp * (k,m)) = (B * (Pk,Pm)) by A18, A24, A37, Th1;

      thus k = m & k <> i & k <> j implies (pBp * (k,k)) = ( 1. F_Real )

      proof

        assume that

         A46: k = m and

         A47: k <> i & k <> j;

        Pk <> 1 & Pk <> 2 by A9, A10, A14, A20, A21, A22, A28, A38, A47, FUNCT_1:def 4;

        then

         A48: Pk > 2 by A1, A41;

        then

        reconsider Pk2 = (Pk - 2) as Nat by NAT_1: 21;

        Pk = (Pk2 + 2) & Pk2 > (2 - 2) by A48, XREAL_1: 8;

        then

         A49: [Pk2, Pk2] in ( Indices ONE) by A16, A18, A27, A30, A44, A46, MATRIXJ1: 27;

        then (ONE * (Pk2,Pk2)) = (B * ((Pk2 + 2),(Pk2 + 2))) by A16, A27, A30, MATRIXJ1: 28;

        hence thesis by A45, A46, A49, MATRIX_1:def 3;

      end;

      

       A50: Pm >= 1 by A43, FINSEQ_1: 1;

      thus k <> m & {k, m} <> {i, j} implies (pBp * (k,m)) = ( 0. F_Real )

      proof

        assume that

         A51: k <> m and

         A52: {k, m} <> {i, j};

        

         A53: Pk <> Pm by A21, A38, A42, A51, FUNCT_1:def 4;

        per cases by A52;

          suppose

           A54: k <> i & k <> j & m <> i & m <> j;

          then Pk <> 1 & Pk <> 2 by A9, A10, A14, A20, A21, A22, A28, A38, FUNCT_1:def 4;

          then

           A55: Pk > 2 by A1, A41;

          Pm <> 1 & Pm <> 2 by A9, A10, A14, A20, A21, A22, A28, A42, A54, FUNCT_1:def 4;

          then

           A56: Pm > 2 by A1, A50;

          then

          reconsider Pk2 = (Pk - 2), Pm2 = (Pm - 2) as Nat by A55, NAT_1: 21;

          

           A57: Pk2 > (2 - 2) by A55, XREAL_1: 8;

          

           A58: Pk = (Pk2 + 2) & Pm = (Pm2 + 2);

          Pm2 > (2 - 2) by A56, XREAL_1: 8;

          then

           A59: [Pk2, Pm2] in ( Indices ONE) by A16, A18, A27, A30, A44, A58, A57, MATRIXJ1: 27;

          then (ONE * (Pk2,Pm2)) = (B * ((Pk2 + 2),(Pm2 + 2))) by A16, A27, A30, MATRIXJ1: 28;

          hence thesis by A45, A53, A59, MATRIX_1:def 3;

        end;

          suppose

           A60: k = i & m <> j;

          then Pm <> 2 by A10, A20, A21, A28, A42, FUNCT_1:def 4;

          then

           A61: Pm > 2 by A1, A9, A14, A50, A53, A60;

          Pk = 1 by A9, A12, A13, A60, FUNCT_1: 34;

          hence thesis by A16, A18, A27, A35, A44, A45, A61, MATRIXJ1: 29;

        end;

          suppose

           A62: k = j & m <> i;

          then Pm <> 1 by A9, A14, A21, A22, A42, FUNCT_1:def 4;

          then

           A63: Pm > 2 by A1, A10, A20, A50, A53, A62;

          Pk = 2 by A10, A12, A19, A62, FUNCT_1: 34;

          hence thesis by A16, A18, A27, A35, A44, A45, A63, MATRIXJ1: 29;

        end;

          suppose

           A64: m = i & k <> j;

          then Pk <> 2 by A10, A20, A21, A28, A38, FUNCT_1:def 4;

          then

           A65: Pk > 2 by A1, A9, A14, A41, A53, A64;

          Pm = 1 by A9, A12, A13, A64, FUNCT_1: 34;

          hence thesis by A16, A18, A27, A35, A44, A45, A65, MATRIXJ1: 29;

        end;

          suppose

           A66: m = j & k <> i;

          then Pk <> 1 by A9, A14, A21, A22, A38, FUNCT_1:def 4;

          then

           A67: Pk > 2 by A1, A10, A20, A41, A53, A66;

          Pm = 2 by A10, A12, A19, A66, FUNCT_1: 34;

          hence thesis by A16, A18, A27, A35, A44, A45, A67, MATRIXJ1: 29;

        end;

      end;

    end;

    begin

    definition

      let n;

      let r be Real;

      let i, j;

      :: MATRTOP3:def3

      func Rotation (i,j,n,r) -> invertible Matrix of n, F_Real means

      : Def3: (it * (i,i)) = ( cos r) & (it * (j,j)) = ( cos r) & (it * (i,j)) = ( sin r) & (it * (j,i)) = ( - ( sin r)) & for k, m st [k, m] in ( Indices it ) holds (k = m & k <> i & k <> j implies (it * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (it * (k,m)) = ( 0. F_Real ));

      existence

      proof

        consider A be Matrix of n, F_Real such that

         A2: ( Det A) = ( 1. F_Real ) and

         A3: (A * (i,i)) = ( cos r) & (A * (j,j)) = ( cos r) & (A * (i,j)) = ( sin r) & (A * (j,i)) = ( - ( sin r)) & for k, m st [k, m] in ( Indices A) holds (k = m & k <> i & k <> j implies (A * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (A * (k,m)) = ( 0. F_Real )) by A1, Lm3;

        ( Det A) <> ( 0. F_Real ) by A2;

        then A is invertible by LAPLACE: 34;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let I1,I2 be invertible Matrix of n, F_Real such that

         A4: (I1 * (i,i)) = ( cos r) & (I1 * (j,j)) = ( cos r) & (I1 * (i,j)) = ( sin r) & (I1 * (j,i)) = ( - ( sin r)) and

         A5: for k, m st [k, m] in ( Indices I1) holds (k = m & k <> i & k <> j implies (I1 * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (I1 * (k,m)) = ( 0. F_Real )) and

         A6: (I2 * (i,i)) = ( cos r) & (I2 * (j,j)) = ( cos r) & (I2 * (i,j)) = ( sin r) & (I2 * (j,i)) = ( - ( sin r)) and

         A7: for k, m st [k, m] in ( Indices I2) holds (k = m & k <> i & k <> j implies (I2 * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (I2 * (k,m)) = ( 0. F_Real ));

        for k, m st [k, m] in ( Indices I1) holds (I1 * (k,m)) = (I2 * (k,m))

        proof

          let k, m;

          assume

           A8: [k, m] in ( Indices I1);

          then

           A9: [k, m] in ( Indices I2) by MATRIX_0: 26;

          per cases ;

            suppose k = m & (k = i or k = j) or k <> m & (k = i & m = j or k = j & m = i);

            hence thesis by A4, A6;

          end;

            suppose

             A10: k = m & k <> i & k <> j;

            then (I1 * (k,m)) = ( 1. F_Real ) by A5, A8;

            hence thesis by A7, A9, A10;

          end;

            suppose

             A11: k <> m & (k = i & m <> j or k = j & m <> i or m = i & k <> j or m = j & k <> i or k <> i & k <> j & m <> i & m <> j);

            then

             A12: {k, m} <> {i, j} by ZFMISC_1: 6;

            then (I1 * (k,m)) = ( 0. F_Real ) by A5, A8, A11;

            hence thesis by A7, A9, A11, A12;

          end;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: MATRTOP3:13

    

     Th13: 1 <= i & i < j & j <= n implies ( Det ( Rotation (i,j,n,r))) = ( 1. F_Real )

    proof

      assume

       A1: 1 <= i & i < j & j <= n;

      then

      consider A be Matrix of n, F_Real such that

       A2: ( Det A) = ( 1. F_Real ) and

       A3: (A * (i,i)) = ( cos r) & (A * (j,j)) = ( cos r) & (A * (i,j)) = ( sin r) & (A * (j,i)) = ( - ( sin r)) & for k, m st [k, m] in ( Indices A) holds (k = m & k <> i & k <> j implies (A * (k,k)) = ( 1. F_Real )) & (k <> m & {k, m} <> {i, j} implies (A * (k,m)) = ( 0. F_Real )) by Lm3;

      ( Det A) <> ( 0. F_Real ) by A2;

      then A is invertible by LAPLACE: 34;

      hence thesis by A1, A2, A3, Def3;

    end;

    theorem :: MATRTOP3:14

    

     Th14: 1 <= i & i < j & j <= n & k in ( Seg n) & k <> i & k <> j implies (( @ p) "*" ( Col (( Rotation (i,j,n,r)),k))) = (p . k)

    proof

      set S = ( Seg n);

      assume that

       A1: 1 <= i & i < j & j <= n and

       A2: k in ( Seg n) and

       A3: k <> i & k <> j;

      set O = ( Rotation (i,j,n,r)), C = ( Col (O,k));

      

       A4: ( Indices O) = [:S, S:] by MATRIX_0: 24;

      then

       A5: [k, k] in ( Indices O) by A2, ZFMISC_1: 87;

      

       A6: ( len O) = n by MATRIX_0: 25;

      then

       A7: ( dom O) = S by FINSEQ_1:def 3;

      ( len C) = n by A6, MATRIX_0:def 8;

      then

       A8: ( dom C) = S by FINSEQ_1:def 3;

       A9:

      now

        let m such that

         A10: m in ( dom C) and

         A11: m <> k;

        

         A12: [m, k] in ( Indices O) by A2, A4, A8, A10, ZFMISC_1: 87;

         not k in {i, j} by A3, TARSKI:def 2;

        then

         A13: {m, k} <> {i, j} by TARSKI:def 2;

        

        thus (C . m) = (O * (m,k)) by A7, A8, A10, MATRIX_0:def 8

        .= ( 0. F_Real ) by A1, A11, A12, A13, Def3;

      end;

      ( len p) = n by CARD_1:def 7;

      then

       A14: ( dom p) = S by FINSEQ_1:def 3;

      (C . k) = (O * (k,k)) by A2, A7, MATRIX_0:def 8

      .= ( 1. F_Real ) by A1, A3, A5, Def3;

      

      hence (p . k) = ( Sum ( mlt (C,( @ p)))) by A2, A8, A9, A14, MATRIX_3: 17

      .= (( @ p) "*" C) by FVSUM_1: 64;

    end;

    theorem :: MATRTOP3:15

    

     Th15: 1 <= i & i < j & j <= n implies (( @ p) "*" ( Col (( Rotation (i,j,n,r)),i))) = (((p . i) * ( cos r)) + ((p . j) * ( - ( sin r))))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= n;

      set O = ( Rotation (i,j,n,r)), C = ( Col (O,i));

      set S = ( Seg n);

      1 <= j by A1, A2, XXREAL_0: 2;

      then

       A4: j in S by A3;

      

       A5: ( len O) = n by MATRIX_0: 25;

      then

       A6: ( dom O) = S by FINSEQ_1:def 3;

      then

       A7: (C . j) = (O * (j,i)) by A4, MATRIX_0:def 8;

      i <= n by A2, A3, XXREAL_0: 2;

      then

       A8: i in S by A1;

      then

       A9: (C . i) = (O * (i,i)) by A6, MATRIX_0:def 8;

      ( len p) = n & ( len C) = n by A5, CARD_1:def 7;

      then

       A10: ( len ( mlt (( @ p),C))) = n by MATRIX_3: 6;

      then

       A11: ( dom ( mlt (( @ p),C))) = S by FINSEQ_1:def 3;

      

       A12: ( Indices O) = [:S, S:] by MATRIX_0: 24;

      for k st k in ( dom ( mlt (( @ p),C))) & k <> i & k <> j holds (( mlt (( @ p),C)) . k) = ( 0. F_Real )

      proof

        let k;

        assume that

         A13: k in ( dom ( mlt (( @ p),C))) and

         A14: k <> i and

         A15: k <> j;

         not k in {i, j} by A14, A15, TARSKI:def 2;

        then

         A16: {k, i} <> {i, j} by TARSKI:def 2;

        reconsider pk = (( @ p) . k) as Element of F_Real by XREAL_0:def 1;

        

         A17: [k, i] in ( Indices O) by A8, A11, A12, A13, ZFMISC_1: 87;

        (C . k) = (O * (k,i)) by A6, A11, A13, MATRIX_0:def 8;

        

        hence (( mlt (( @ p),C)) . k) = (pk * (O * (k,i))) by A13, FVSUM_1: 60

        .= (pk * ( 0. F_Real )) by A1, A2, A3, A14, A16, A17, Def3

        .= ( 0. F_Real );

      end;

      then

       A18: ( Sum ( mlt (( @ p),C))) = ((( mlt (( @ p),C)) /. i) + (( mlt (( @ p),C)) /. j)) by A2, A4, A8, A11, MATRIX15: 7;

      

       A19: i in ( dom ( mlt (( @ p),C))) by A8, A10, FINSEQ_1:def 3;

      reconsider pii = (( @ p) . i), pj = (( @ p) . j) as Element of F_Real by XREAL_0:def 1;

      

       A20: (( mlt (( @ p),C)) /. i) = (( mlt (( @ p),C)) . i) by A8, A11, PARTFUN1:def 6

      .= (pii * (O * (i,i))) by A9, A19, FVSUM_1: 60

      .= ((p . i) * ( cos r)) by A1, A2, A3, Def3;

      (( mlt (( @ p),C)) /. j) = (( mlt (( @ p),C)) . j) by A4, A11, PARTFUN1:def 6

      .= (pj * (O * (j,i))) by A4, A7, A11, FVSUM_1: 60

      .= ((p . j) * ( - ( sin r))) by A1, A2, A3, Def3;

      hence thesis by A18, A20;

    end;

    theorem :: MATRTOP3:16

    

     Th16: 1 <= i & i < j & j <= n implies (( @ p) "*" ( Col (( Rotation (i,j,n,r)),j))) = (((p . i) * ( sin r)) + ((p . j) * ( cos r)))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= n;

      set O = ( Rotation (i,j,n,r)), C = ( Col (O,j));

      set S = ( Seg n);

      1 <= j by A1, A2, XXREAL_0: 2;

      then

       A4: j in S by A3;

      

       A5: ( len O) = n by MATRIX_0: 25;

      then

       A6: ( dom O) = S by FINSEQ_1:def 3;

      then

       A7: (C . j) = (O * (j,j)) by A4, MATRIX_0:def 8;

      

       A8: i <= n by A2, A3, XXREAL_0: 2;

      then

       A9: i in S by A1;

      then

       A10: (C . i) = (O * (i,j)) by A6, MATRIX_0:def 8;

      ( len p) = n & ( len C) = n by A5, CARD_1:def 7;

      then ( len ( mlt (( @ p),C))) = n by MATRIX_3: 6;

      then

       A11: ( dom ( mlt (( @ p),C))) = S by FINSEQ_1:def 3;

      then

       A12: i in ( dom ( mlt (( @ p),C))) by A1, A8;

      

       A13: ( Indices O) = [:S, S:] by MATRIX_0: 24;

      for k st k in ( dom ( mlt (( @ p),C))) & k <> i & k <> j holds (( mlt (( @ p),C)) . k) = ( 0. F_Real )

      proof

        let k;

        assume that

         A14: k in ( dom ( mlt (( @ p),C))) and

         A15: k <> i and

         A16: k <> j;

         not k in {i, j} by A15, A16, TARSKI:def 2;

        then

         A17: {k, j} <> {i, j} by TARSKI:def 2;

        reconsider pk = (( @ p) . k) as Element of F_Real by XREAL_0:def 1;

        

         A18: [k, j] in ( Indices O) by A4, A11, A13, A14, ZFMISC_1: 87;

        (C . k) = (O * (k,j)) by A6, A11, A14, MATRIX_0:def 8;

        

        hence (( mlt (( @ p),C)) . k) = (pk * (O * (k,j))) by A14, FVSUM_1: 60

        .= (pk * ( 0. F_Real )) by A1, A2, A3, A16, A17, A18, Def3

        .= ( 0. F_Real );

      end;

      then

       A19: ( Sum ( mlt (( @ p),C))) = ((( mlt (( @ p),C)) /. i) + (( mlt (( @ p),C)) /. j)) by A2, A4, A9, A11, MATRIX15: 7;

      reconsider pii = (( @ p) . i), pj = (( @ p) . j) as Element of F_Real by XREAL_0:def 1;

      

       A20: (( mlt (( @ p),C)) /. i) = (( mlt (( @ p),C)) . i) by A9, A11, PARTFUN1:def 6

      .= (pii * (O * (i,j))) by A10, A12, FVSUM_1: 60

      .= ((p . i) * ( sin r)) by A1, A2, A3, Def3;

      (( mlt (( @ p),C)) /. j) = (( mlt (( @ p),C)) . j) by A4, A11, PARTFUN1:def 6

      .= (pj * (O * (j,j))) by A4, A7, A11, FVSUM_1: 60

      .= ((p . j) * ( cos r)) by A1, A2, A3, Def3;

      hence thesis by A19, A20;

    end;

    theorem :: MATRTOP3:17

    

     Th17: 1 <= i & i < j & j <= n implies (( Rotation (i,j,n,r1)) * ( Rotation (i,j,n,r2))) = ( Rotation (i,j,n,(r1 + r2)))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= n;

      set S = ( Seg n);

      1 <= j by A1, A2, XXREAL_0: 2;

      then

       A4: j in S by A3;

      set O1 = ( Rotation (i,j,n,r1));

      set O2 = ( Rotation (i,j,n,r2));

      set O = ( Rotation (i,j,n,(r1 + r2)));

      set O12 = (O1 * O2);

      

       A5: ( width O1) = n by MATRIX_0: 24;

      i <= n by A2, A3, XXREAL_0: 2;

      then

       A6: i in S by A1;

      

       A7: ( Indices O1) = [:S, S:] by MATRIX_0: 24;

      

       A8: ( Indices O12) = [:S, S:] by MATRIX_0: 24;

      

       A9: ( Indices O) = [:S, S:] by MATRIX_0: 24;

      

       A10: ( len O2) = n by MATRIX_0: 25;

      for k, m st [k, m] in ( Indices O12) holds (O12 * (k,m)) = (O * (k,m))

      proof

        let k, m;

        assume

         A11: [k, m] in ( Indices O12);

        then

         A12: k in S by A8, ZFMISC_1: 87;

        

         A13: (O12 * (k,m)) = (( Line (O1,k)) "*" ( Col (O2,m))) by A5, A10, A11, MATRIX_3:def 4;

        ( len ( @ ( Line (O1,k)))) = n by A5, CARD_1:def 7;

        then

        reconsider L = ( @ ( Line (O1,k))) as Element of ( TOP-REAL n) by TOPREAL3: 46;

        

         A14: m in S by A8, A11, ZFMISC_1: 87;

        then

         A15: (L . m) = (O1 * (k,m)) by A5, MATRIX_0:def 7;

        

         A16: ( @ L) = ( Line (O1,k));

        

         A17: (L . i) = (O1 * (k,i)) by A5, A6, MATRIX_0:def 7;

        

         A18: (L . j) = (O1 * (k,j)) by A4, A5, MATRIX_0:def 7;

        per cases ;

          suppose

           A19: m = i;

          then

           A20: (( Line (O1,k)) "*" ( Col (O2,m))) = (((L . i) * ( cos r2)) + ((L . j) * ( - ( sin r2)))) by A1, A2, A3, A16, Th15;

          per cases ;

            suppose

             A21: k = i;

            

            hence (O12 * (k,m)) = ((( cos r1) * ( cos r2)) + ((L . j) * ( - ( sin r2)))) by A1, A2, A3, A13, A17, A20, Def3

            .= ((( cos r1) * ( cos r2)) + (( sin r1) * ( - ( sin r2)))) by A1, A2, A3, A18, A21, Def3

            .= ((( cos r1) * ( cos r2)) - (( sin r1) * ( sin r2)))

            .= ( cos (r1 + r2)) by SIN_COS: 75

            .= (O * (k,m)) by A1, A2, A3, A19, A21, Def3;

          end;

            suppose

             A22: k = j;

            

            hence (O12 * (k,m)) = ((( - ( sin r1)) * ( cos r2)) + ((L . j) * ( - ( sin r2)))) by A1, A2, A3, A13, A17, A20, Def3

            .= ((( - ( sin r1)) * ( cos r2)) + (( cos r1) * ( - ( sin r2)))) by A1, A2, A3, A18, A22, Def3

            .= ( - ((( sin r1) * ( cos r2)) + (( cos r1) * ( sin r2))))

            .= ( - ( sin (r1 + r2))) by SIN_COS: 75

            .= (O * (k,m)) by A1, A2, A3, A19, A22, Def3;

          end;

            suppose k <> j & k <> i;

            then not k in {i, j} by TARSKI:def 2;

            then

             A23: {k, i} <> {i, j} & {k, j} <> {i, j} by TARSKI:def 2;

            

             A24: [k, j] in [:S, S:] by A4, A12, ZFMISC_1: 87;

            

             A25: [k, i] in [:S, S:] by A6, A12, ZFMISC_1: 87;

            then (O1 * (k,i)) = ( 0. F_Real ) by A1, A2, A3, A7, A23, Def3;

            

            hence (O12 * (k,m)) = (( 0 * ( cos r2)) + ( 0 * ( - ( sin r2)))) by A1, A2, A3, A7, A13, A17, A18, A20, A23, A24, Def3

            .= (O * (k,m)) by A1, A2, A3, A9, A19, A23, A25, Def3;

          end;

        end;

          suppose

           A26: m = j;

          then

           A27: (( Line (O1,k)) "*" ( Col (O2,m))) = (((L . i) * ( sin r2)) + ((L . j) * ( cos r2))) by A1, A2, A3, A16, Th16;

          per cases ;

            suppose

             A28: k = i;

            

            hence (O12 * (k,m)) = ((( cos r1) * ( sin r2)) + ((L . j) * ( cos r2))) by A1, A2, A3, A13, A17, A27, Def3

            .= ((( cos r1) * ( sin r2)) + (( sin r1) * ( cos r2))) by A1, A2, A3, A18, A28, Def3

            .= ( sin (r1 + r2)) by SIN_COS: 75

            .= (O * (k,m)) by A1, A2, A3, A26, A28, Def3;

          end;

            suppose

             A29: k = j;

            

            hence (O12 * (k,m)) = ((( - ( sin r1)) * ( sin r2)) + ((L . j) * ( cos r2))) by A1, A2, A3, A13, A17, A27, Def3

            .= ((( cos r1) * ( cos r2)) - (( sin r1) * ( sin r2))) by A1, A2, A3, A18, A29, Def3

            .= ( cos (r1 + r2)) by SIN_COS: 75

            .= (O * (k,m)) by A1, A2, A3, A26, A29, Def3;

          end;

            suppose k <> j & k <> i;

            then not k in {i, j} by TARSKI:def 2;

            then

             A30: {k, i} <> {i, j} & {k, j} <> {i, j} by TARSKI:def 2;

            

             A31: [k, j] in [:S, S:] by A4, A12, ZFMISC_1: 87;

             [k, i] in [:S, S:] by A6, A12, ZFMISC_1: 87;

            then (O1 * (k,i)) = ( 0. F_Real ) by A1, A2, A3, A7, A30, Def3;

            

            hence (O12 * (k,m)) = (( 0 * ( sin r2)) + ( 0 * ( cos r2))) by A1, A2, A3, A7, A13, A17, A18, A27, A30, A31, Def3

            .= (O * (k,m)) by A1, A2, A3, A9, A26, A30, A31, Def3;

          end;

        end;

          suppose

           A32: m <> i & m <> j;

          then

           A33: (O12 * (k,m)) = (L . m) by A1, A2, A3, A13, A14, A16, Th14;

          

           A34: [k, m] in [:S, S:] by A11, MATRIX_0: 24;

          per cases ;

            suppose

             A35: k = m;

            then (O1 * (k,m)) = ( 1. F_Real ) by A1, A2, A3, A7, A8, A11, A32, Def3;

            hence thesis by A1, A2, A3, A9, A15, A32, A33, A34, A35, Def3;

          end;

            suppose

             A36: k <> m;

             not m in {i, j} by A32, TARSKI:def 2;

            then

             A37: {k, m} <> {i, j} by TARSKI:def 2;

            then (O1 * (k,m)) = ( 0. F_Real ) by A1, A2, A3, A7, A8, A11, A36, Def3;

            hence thesis by A1, A2, A3, A9, A15, A33, A34, A36, A37, Def3;

          end;

        end;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    

     Lm4: 1 <= i & i < j & j <= n implies (( Rotation (i,j,n,r)) @ ) = ( Rotation (i,j,n,( - r)))

    proof

      set O1 = ( Rotation (i,j,n,r)), O2 = ( Rotation (i,j,n,( - r)));

      set S = ( Seg n);

      assume

       A1: 1 <= i & i < j & j <= n;

      

       A2: ( Indices O2) = [:S, S:] by MATRIX_0: 24;

      

       A3: ( Indices O1) = [:S, S:] by MATRIX_0: 24;

      

       A4: ( Indices (O1 @ )) = [:S, S:] by MATRIX_0: 24;

      for k, m st [k, m] in [:S, S:] holds ((O1 @ ) * (k,m)) = (O2 * (k,m))

      proof

        

         A5: ( cos r) = ( cos ( - r)) by SIN_COS: 31;

        let k, m;

        

         A6: ( - ( sin r)) = ( sin ( - r)) by SIN_COS: 31;

        assume

         A7: [k, m] in [:S, S:];

        then

         A8: [m, k] in [:S, S:] by A3, A4, MATRIX_0:def 6;

        then

         A9: ((O1 @ ) * (k,m)) = (O1 * (m,k)) by A3, MATRIX_0:def 6;

        per cases ;

          suppose

           A10: k = m & k = i;

          then (O1 * (m,k)) = ( cos r) by A1, Def3;

          hence thesis by A1, A5, A9, A10, Def3;

        end;

          suppose

           A11: k = m & k = j;

          then (O1 * (m,k)) = ( cos r) by A1, Def3;

          hence thesis by A1, A5, A9, A11, Def3;

        end;

          suppose

           A12: k = m & k <> i & k <> j;

          then (O1 * (m,k)) = ( 1. F_Real ) by A1, A3, A7, Def3;

          hence thesis by A1, A2, A7, A9, A12, Def3;

        end;

          suppose

           A13: k <> m & k = i & m = j;

          then (O1 * (m,k)) = ( - ( sin r)) by A1, Def3;

          hence thesis by A1, A6, A9, A13, Def3;

        end;

          suppose

           A14: k <> m & k = i & m <> j;

          then not m in {i, j} by TARSKI:def 2;

          then

           A15: {m, k} <> {i, j} by TARSKI:def 2;

          then (O1 * (m,k)) = ( 0. F_Real ) by A1, A3, A8, A14, Def3;

          hence thesis by A1, A2, A7, A9, A14, A15, Def3;

        end;

          suppose

           A16: k <> m & k = j & m = i;

          then (O2 * (k,m)) = ( - ( sin ( - r))) by A1, Def3;

          hence thesis by A1, A6, A9, A16, Def3;

        end;

          suppose

           A17: k <> m & k = j & m <> i;

          then not m in {i, j} by TARSKI:def 2;

          then

           A18: {m, k} <> {i, j} by TARSKI:def 2;

          then (O1 * (m,k)) = ( 0. F_Real ) by A1, A3, A8, A17, Def3;

          hence thesis by A1, A2, A7, A9, A17, A18, Def3;

        end;

          suppose

           A19: k <> m & k <> j & k <> i;

          then not k in {i, j} by TARSKI:def 2;

          then

           A20: {m, k} <> {i, j} by TARSKI:def 2;

          then (O1 * (m,k)) = ( 0. F_Real ) by A1, A3, A8, A19, Def3;

          hence thesis by A1, A2, A7, A9, A19, A20, Def3;

        end;

          suppose

           A21: k <> m & m <> j & m <> i;

          then not m in {i, j} by TARSKI:def 2;

          then

           A22: {m, k} <> {i, j} by TARSKI:def 2;

          then (O1 * (m,k)) = ( 0. F_Real ) by A1, A3, A8, A21, Def3;

          hence thesis by A1, A2, A7, A9, A21, A22, Def3;

        end;

      end;

      hence thesis by A4, MATRIX_0: 27;

    end;

    theorem :: MATRTOP3:18

    

     Th18: 1 <= i & i < j & j <= n implies ( Rotation (i,j,n, 0 )) = ( 1. ( F_Real ,n))

    proof

      set O = ( Rotation (i,j,n, 0 ));

      assume

       A1: 1 <= i & i < j & j <= n;

      

       A2: for k, m st [k, m] in ( Indices O) & k <> m holds (O * (k,m)) = ( 0. F_Real )

      proof

        let k, m;

        assume that

         A3: [k, m] in ( Indices O) and

         A4: k <> m;

        per cases ;

          suppose k = i & m = j or k = j & m = i;

          then (O * (k,m)) = ( sin 0 ) or (O * (k,m)) = ( - ( sin 0 )) by A1, Def3;

          hence thesis by SIN_COS: 31;

        end;

          suppose k = i & m <> j;

          then not m in {i, j} by A4, TARSKI:def 2;

          then {k, m} <> {i, j} by TARSKI:def 2;

          hence thesis by A1, A3, A4, Def3;

        end;

          suppose k = j & m <> i;

          then not m in {i, j} by A4, TARSKI:def 2;

          then {k, m} <> {i, j} by TARSKI:def 2;

          hence thesis by A1, A3, A4, Def3;

        end;

          suppose m = i & k <> j;

          then not k in {i, j} by A4, TARSKI:def 2;

          then {k, m} <> {i, j} by TARSKI:def 2;

          hence thesis by A1, A3, A4, Def3;

        end;

          suppose m = j & k <> i;

          then not k in {i, j} by A4, TARSKI:def 2;

          then {k, m} <> {i, j} by TARSKI:def 2;

          hence thesis by A1, A3, A4, Def3;

        end;

          suppose k <> i & k <> j & m <> i & m <> j;

          then not m in {i, j} by TARSKI:def 2;

          then {k, m} <> {i, j} by TARSKI:def 2;

          hence thesis by A1, A3, A4, Def3;

        end;

      end;

      for k st [k, k] in ( Indices O) holds (O * (k,k)) = ( 1. F_Real )

      proof

        let k;

        assume

         A5: [k, k] in ( Indices O);

        k = i or k = j or k <> i & k <> j;

        hence thesis by A1, A5, Def3, SIN_COS: 31;

      end;

      hence thesis by A2, MATRIX_1:def 3;

    end;

    

     Lm5: 1 <= i & i < j & j <= n implies (( Rotation (i,j,n,r)) ~ ) = ( Rotation (i,j,n,( - r)))

    proof

      assume

       A1: 1 <= i & i < j & j <= n;

      

      then

       A2: (( Rotation (i,j,n,r)) * ( Rotation (i,j,n,( - r)))) = ( Rotation (i,j,n,(r + ( - r)))) by Th17

      .= ( 1. ( F_Real ,n)) by A1, Th18;

      (( Rotation (i,j,n,( - r))) * ( Rotation (i,j,n,r))) = ( Rotation (i,j,n,(( - r) + r))) by A1, Th17

      .= ( 1. ( F_Real ,n)) by A1, Th18;

      then ( Rotation (i,j,n,r)) is_reverse_of ( Rotation (i,j,n,( - r))) by A2, MATRIX_6:def 2;

      hence thesis by MATRIX_6:def 4;

    end;

    theorem :: MATRTOP3:19

    

     Th19: 1 <= i & i < j & j <= n implies ( Rotation (i,j,n,r)) is Orthogonal & (( Rotation (i,j,n,r)) ~ ) = ( Rotation (i,j,n,( - r)))

    proof

      assume 1 <= i & i < j & j <= n;

      then (( Rotation (i,j,n,r)) ~ ) = ( Rotation (i,j,n,( - r))) & (( Rotation (i,j,n,r)) @ ) = ( Rotation (i,j,n,( - r))) by Lm4, Lm5;

      hence thesis by MATRIX_6:def 7;

    end;

    theorem :: MATRTOP3:20

    

     Th20: 1 <= i & i < j & j <= n & k <> i & k <> j implies ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . k) = (p . k)

    proof

      set O = ( Rotation (i,j,n,r)), M = ( Mx2Tran O), Mp = (M . p), S = ( Seg n);

      assume

       A1: 1 <= i & i < j & j <= n & k <> i & k <> j;

      ( len Mp) = n by CARD_1:def 7;

      then

       A2: ( dom Mp) = S by FINSEQ_1:def 3;

      ( len p) = n by CARD_1:def 7;

      then

       A3: ( dom p) = S by FINSEQ_1:def 3;

      per cases ;

        suppose

         A4: k in S;

        then 1 <= k & k <= n by FINSEQ_1: 1;

        

        hence (Mp . k) = (( @ p) "*" ( Col (O,k))) by MATRTOP1: 18

        .= (p . k) by A1, A4, Th14;

      end;

        suppose

         A5: not k in S;

        then (Mp . k) = {} by A2, FUNCT_1:def 2;

        hence thesis by A3, A5, FUNCT_1:def 2;

      end;

    end;

    theorem :: MATRTOP3:21

    

     Th21: 1 <= i & i < j & j <= n implies ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) = (((p . i) * ( cos r)) + ((p . j) * ( - ( sin r))))

    proof

      set O = ( Rotation (i,j,n,r)), M = ( Mx2Tran O), Mp = (M . p), S = ( Seg n);

      assume that

       A1: 1 <= i and

       A2: i < j & j <= n;

      i <= n by A2, XXREAL_0: 2;

      

      hence (Mp . i) = (( @ p) "*" ( Col (O,i))) by A1, MATRTOP1: 18

      .= (((p . i) * ( cos r)) + ((p . j) * ( - ( sin r)))) by A1, A2, Th15;

    end;

    theorem :: MATRTOP3:22

    

     Th22: 1 <= i & i < j & j <= n implies ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . j) = (((p . i) * ( sin r)) + ((p . j) * ( cos r)))

    proof

      set O = ( Rotation (i,j,n,r)), M = ( Mx2Tran O), Mp = (M . p), S = ( Seg n);

      assume that

       A1: 1 <= i & i < j and

       A2: j <= n;

      1 <= j by A1, XXREAL_0: 2;

      

      hence (Mp . j) = (( @ p) "*" ( Col (O,j))) by A2, MATRTOP1: 18

      .= (((p . i) * ( sin r)) + ((p . j) * ( cos r))) by A1, A2, Th16;

    end;

    theorem :: MATRTOP3:23

    

     Th23: 1 <= i & i < j & j <= n implies (( Mx2Tran ( Rotation (i,j,n,r))) . p) = (((((p | (i -' 1)) ^ <*(((p . i) * ( cos r)) + ((p . j) * ( - ( sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * ( sin r)) + ((p . j) * ( cos r)))*>) ^ (p /^ j))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= n;

      set M = ( Mx2Tran ( Rotation (i,j,n,r))), Mp = (M . p), i1 = (i -' 1), ji = (j -' i);

      

       A4: i < n by A2, A3, XXREAL_0: 2;

      

       A5: i1 < (i1 + 1) & i1 = (i - 1) by A1, NAT_1: 13, XREAL_1: 233;

       A6:

      now

        let k;

        assume that 1 <= k and

         A7: k <= i1;

        

         A8: ((Mp | i1) . k) = (Mp . k) & ((p | i1) . k) = (p . k) by A7, FINSEQ_3: 112;

        k < i by A5, A7, XXREAL_0: 2;

        hence ((Mp | i1) . k) = ((p | i1) . k) by A1, A2, A3, A8, Th20;

      end;

      

       A9: ( len Mp) = n by CARD_1:def 7;

      then

       A10: ( len (Mp | i1)) = i1 by A5, A4, FINSEQ_1: 59, XXREAL_0: 2;

      

       A11: ( len p) = n by CARD_1:def 7;

      then

       A12: ( len (p /^ i)) = (n - i) by A4, RFINSEQ:def 1;

      

       A13: ji = (j - i) by A2, XREAL_1: 233;

      then

       A14: (ji -' 1) < ((ji -' 1) + 1) & ji <= (n - i) by A3, NAT_1: 13, XREAL_1: 6;

      (j - i) > (i - i) by A2, XREAL_1: 8;

      then

       A15: (ji -' 1) = (ji - 1) by A13, NAT_1: 14, XREAL_1: 233;

      

       A16: ( len (p /^ j)) = (n - j) by A3, A11, RFINSEQ:def 1;

      

       A17: ( len (Mp /^ i)) = (n - i) by A9, A4, RFINSEQ:def 1;

      then

       A18: ( len ((Mp /^ i) | (ji -' 1))) = (ji -' 1) by A14, A15, FINSEQ_1: 59, XXREAL_0: 2;

      

       A19: (ji -' 1) < (n - i) by A14, A15, XXREAL_0: 2;

       A20:

      now

        let k;

        assume that

         A21: 1 <= k and

         A22: k <= (ji -' 1);

        

         A23: (((p /^ i) | (ji -' 1)) . k) = ((p /^ i) . k) by A22, FINSEQ_3: 112;

        

         A24: k <= (n - i) by A19, A22, XXREAL_0: 2;

        then k in ( dom (Mp /^ i)) by A17, A21, FINSEQ_3: 25;

        then

         A25: ((Mp /^ i) . k) = (Mp . (i + k)) by A9, A4, RFINSEQ:def 1;

        k < ((ji -' 1) + 1) by A22, NAT_1: 13;

        then

         A26: (i + k) < (i + ji) by A15, XREAL_1: 8;

        k in ( dom (p /^ i)) by A12, A21, A24, FINSEQ_3: 25;

        then

         A27: ((p /^ i) . k) = (p . (i + k)) by A11, A4, RFINSEQ:def 1;

        (k + i) <> i & (((Mp /^ i) | (ji -' 1)) . k) = ((Mp /^ i) . k) by A21, A22, FINSEQ_3: 112, NAT_1: 14;

        hence (((Mp /^ i) | (ji -' 1)) . k) = (((p /^ i) | (ji -' 1)) . k) by A1, A2, A3, A13, A25, A26, A27, A23, Th20;

      end;

      ( len ((p /^ i) | (ji -' 1))) = (ji -' 1) by A14, A15, A12, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A28: ((Mp /^ i) | (ji -' 1)) = ((p /^ i) | (ji -' 1)) by A20, A18;

      

       A29: ( len (Mp /^ j)) = (n - j) by A3, A9, RFINSEQ:def 1;

      now

        let k;

        assume that

         A30: 1 <= k and

         A31: k <= (n - j);

        k in ( dom (Mp /^ j)) by A29, A30, A31, FINSEQ_3: 25;

        then

         A32: ((Mp /^ j) . k) = (Mp . (j + k)) by A3, A9, RFINSEQ:def 1;

        k in ( dom (p /^ j)) by A16, A30, A31, FINSEQ_3: 25;

        then

         A33: ((p /^ j) . k) = (p . (j + k)) by A3, A11, RFINSEQ:def 1;

        (j + k) >= j & (j + k) <> j by A30, NAT_1: 11, NAT_1: 14;

        hence ((Mp /^ j) . k) = ((p /^ j) . k) by A1, A2, A3, A32, A33, Th20;

      end;

      then

       A34: (Mp /^ j) = (p /^ j) by A16, A29;

      ( len (p | i1)) = i1 by A5, A11, A4, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A35: (Mp | i1) = (p | i1) by A6, A10;

      

       A36: (Mp . i) = (((p . i) * ( cos r)) + ((p . j) * ( - ( sin r)))) by A1, A2, A3, Th21;

      Mp = ( @ ( @ Mp));

      then Mp = (((((Mp | i1) ^ <*(Mp . i)*>) ^ ((Mp /^ i) | ((j -' i) -' 1))) ^ <*(Mp . j)*>) ^ (Mp /^ j)) by A1, A2, A3, A9, FINSEQ_7: 1;

      hence thesis by A1, A2, A3, A34, A28, A35, A36, Th22;

    end;

    theorem :: MATRTOP3:24

    

     Th24: 1 <= i & i < j & j <= n & (s ^2 ) <= (((p . i) ^2 ) + ((p . j) ^2 )) implies ex r st ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) = s

    proof

      set pk = (p . i), pj = (p . j), pkj = ((pk ^2 ) + (pj ^2 )), P = ( sqrt pkj);

      assume that

       A1: 1 <= i & i < j & j <= n and

       A2: (s ^2 ) <= (((p . i) ^2 ) + ((p . j) ^2 ));

      

       A3: 0 <= (pk * pk) & 0 <= (pj * pj) by XREAL_1: 63;

      per cases ;

        suppose

         A4: pk <> 0 or pj <> 0 ;

        

         A5: 0 <= (pk * pk) by XREAL_1: 63;

        

         A6: P > 0 by A3, A4, SQUARE_1: 25;

        then

         A7: ((s / P) * P) = s by XCMPLX_1: 87;

        

         A8: 0 <= (pj * pj) by XREAL_1: 63;

        then ((pk ^2 ) + 0 ) <= ((pk ^2 ) + (pj ^2 )) by XREAL_1: 6;

        then

         A9: ( sqrt (pk ^2 )) <= P by A5, SQUARE_1: 26;

        now

          per cases ;

            suppose

             A10: pk >= 0 ;

            then

             A11: pk <= P by A9, SQUARE_1: 22;

            then (pk / P) <= 1 by A6, XREAL_1: 185;

            hence (pk / P) in [.( - 1), 1.] by A10, A11, XXREAL_1: 1;

          end;

            suppose

             A12: pk <= 0 ;

            then ( - pk) <= P by A9, SQUARE_1: 23;

            then ( - 1) <= (pk / P) by A6, XREAL_1: 194;

            hence (pk / P) in [.( - 1), 1.] by A6, A12, XXREAL_1: 1;

          end;

        end;

        then

        consider x be object such that

         A13: x in ( dom sin ) and x in [.( - ( PI / 2)), ( PI / 2).] and

         A14: ( sin . x) = (pk / P) by FUNCT_1:def 6, SIN_COS6: 45;

        

         A15: (P * P) = (P ^2 )

        .= pkj by A5, A8, SQUARE_1:def 2;

         0 <= (s * s) by XREAL_1: 63;

        then

         A16: ( sqrt (s ^2 )) <= P by A2, SQUARE_1: 26;

        now

          per cases ;

            suppose

             A17: s >= 0 ;

            then

             A18: s <= P by A16, SQUARE_1: 22;

            then (s / P) <= 1 by A6, XREAL_1: 185;

            hence (s / P) in [.( - 1), 1.] by A17, A18, XXREAL_1: 1;

          end;

            suppose

             A19: s <= 0 ;

            then ( - s) <= P by A16, SQUARE_1: 23;

            then ( - 1) <= (s / P) by A6, XREAL_1: 194;

            hence (s / P) in [.( - 1), 1.] by A6, A19, XXREAL_1: 1;

          end;

        end;

        then

        consider y be object such that y in ( dom sin ) and

         A20: y in [.( - ( PI / 2)), ( PI / 2).] and

         A21: ( sin . y) = (s / P) by FUNCT_1:def 6, SIN_COS6: 45;

        reconsider y as Real by A20;

        

         A22: ((P * pk) / P) = pk by A6, XCMPLX_1: 89;

        reconsider x as Element of REAL by A13, FUNCT_2:def 1;

        

         A23: ( sin . x) = ( sin x) by SIN_COS:def 17;

        ((pk / P) * (pk / P)) = ((pk * pk) / pkj) by A15, XCMPLX_1: 76;

        then ((( cos x) * ( cos x)) + ((pk * pk) / pkj)) = 1 by A14, A23, SIN_COS: 29;

        

        then (( cos x) * ( cos x)) = (1 - ((pk * pk) / pkj))

        .= ((pkj / pkj) - ((pk * pk) / pkj)) by A3, A4, XCMPLX_1: 60

        .= ((pj * pj) / pkj)

        .= ((pj / P) ^2 ) by A15, XCMPLX_1: 76;

        then

         A24: (( cos x) ^2 ) = ((pj / P) ^2 );

        per cases by A24, SQUARE_1: 40;

          suppose

           A25: ( cos x) = (pj / P);

          take r = (x - y);

          ( - ( sin y)) = ( sin (( - x) + r)) by SIN_COS: 31

          .= ((( sin ( - x)) * ( cos r)) + (( cos ( - x)) * ( sin r))) by SIN_COS: 75

          .= ((( - ( sin x)) * ( cos r)) + (( cos ( - x)) * ( sin r))) by SIN_COS: 31

          .= (( - (( sin x) * ( cos r))) + (( cos x) * ( sin r))) by SIN_COS: 31

          .= (( - (( sin x) * ( cos r))) + ( - (( cos x) * ( - ( sin r)))));

          then ( sin y) = ((( sin x) * ( cos r)) + (( cos x) * ( - ( sin r))));

          

          hence s = (P * (((pk / P) * ( cos r)) + ((pj / P) * ( - ( sin r))))) by A7, A14, A21, A23, A25, SIN_COS:def 17

          .= ((((P * pk) / P) * ( cos r)) + (((P * pj) / P) * ( - ( sin r))))

          .= ((pk * ( cos r)) + (pj * ( - ( sin r)))) by A6, A22, XCMPLX_1: 89

          .= ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) by A1, Th21;

        end;

          suppose

           A26: ( cos x) = ( - (pj / P));

          take r = (y - x);

          ( sin y) = ( sin (x + r))

          .= ((( sin x) * ( cos r)) + (( cos x) * ( sin r))) by SIN_COS: 75

          .= (((pk / P) * ( cos r)) + ((pj / P) * ( - ( sin r)))) by A14, A26, SIN_COS:def 17;

          

          hence s = (P * (((pk / P) * ( cos r)) + ((pj / P) * ( - ( sin r))))) by A7, A21, SIN_COS:def 17

          .= ((((P * pk) / P) * ( cos r)) + (((P * pj) / P) * ( - ( sin r))))

          .= ((pk * ( cos r)) + (pj * ( - ( sin r)))) by A6, A22, XCMPLX_1: 89

          .= ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) by A1, Th21;

        end;

      end;

        suppose

         A27: pk = 0 & pj = 0 ;

        take r = 0 ;

        set M = ( Mx2Tran ( Rotation (i,j,n,r)));

        M = ( Mx2Tran ( 1. ( F_Real ,n))) by A1, Th18;

        then

         A28: M = ( id ( TOP-REAL n)) by MATRTOP1: 33;

        s = 0 by A2, A27, XREAL_1: 63;

        hence thesis by A27, A28;

      end;

    end;

    

     Lm6: 1 <= i & i < j & j <= n implies ((((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) * ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i)) + (((( Mx2Tran ( Rotation (i,j,n,r))) . p) . j) * ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . j))) = (((p . i) * (p . i)) + ((p . j) * (p . j)))

    proof

      set pk = (p . i), pj = (p . j), pkj = ((pk ^2 ) + (pj ^2 ));

      set M = ( Mx2Tran ( Rotation (i,j,n,r))), S = ( sin r), C = ( cos r), Mp = (M . p);

      

       A1: ((C * C) + (S * S)) = 1 by SIN_COS: 29;

      assume

       A2: 1 <= i & i < j & j <= n;

      then (Mp . i) = ((pk * C) + (pj * ( - S))) by Th21;

      then

       A3: ((Mp . i) * (Mp . i)) = (((((pk * pk) * C) * C) - ((((2 * pk) * pj) * C) * S)) + (((pj * pj) * S) * S));

      (Mp . j) = ((pk * S) + (pj * C)) by A2, Th22;

      then ((Mp . j) * (Mp . j)) = (((((pk * pk) * S) * S) + ((2 * (pk * pj)) * (C * S))) + ((pj * pj) * (C * C)));

      

      hence (((Mp . i) * (Mp . i)) + ((Mp . j) * (Mp . j))) = (((pk * pk) * ((C * C) + (S * S))) + ((pj * pj) * ((C * C) + (S * S)))) by A3

      .= ((pk * pk) + (pj * pj)) by A1;

    end;

    theorem :: MATRTOP3:25

    

     Th25: 1 <= i & i < j & j <= n & (s ^2 ) <= (((p . i) ^2 ) + ((p . j) ^2 )) implies ex r st ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . j) = s

    proof

      set pk = (p . i), pj = (p . j), pkj = ((pk ^2 ) + (pj ^2 )), ps = (pkj - (s ^2 ));

      assume that

       A1: 1 <= i & i < j & j <= n and

       A2: (s ^2 ) <= ((pk ^2 ) + (pj ^2 ));

       0 <= (s * s) by XREAL_1: 63;

      then

       A3: ps <= (pkj - 0 ) by XREAL_1: 6;

      

       A4: ((s ^2 ) - (s ^2 )) <= ps by A2, XREAL_1: 6;

      then (( sqrt ps) ^2 ) = ps by SQUARE_1:def 2;

      then

      consider r such that

       A5: ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) = ( sqrt ps) by A1, A3, Th24;

      set M = ( Mx2Tran ( Rotation (i,j,n,r))), Mp = (M . p);

      pkj = ((( sqrt ps) ^2 ) + ((Mp . j) * (Mp . j))) by A5, A1, Lm6

      .= (ps + ((Mp . j) * (Mp . j))) by A4, SQUARE_1:def 2;

      then

       A6: (s ^2 ) = ((Mp . j) ^2 );

      per cases by A6, SQUARE_1: 40;

        suppose (Mp . j) = s;

        hence thesis;

      end;

        suppose

         A7: (Mp . j) = ( - s);

        take R = (r + PI );

        

        thus ((( Mx2Tran ( Rotation (i,j,n,R))) . p) . j) = (((p . i) * ( sin R)) + ((p . j) * ( cos R))) by A1, Th22

        .= (((p . i) * ( - ( sin r))) + ((p . j) * ( cos R))) by SIN_COS: 79

        .= (((p . i) * ( - ( sin r))) + ((p . j) * ( - ( cos r)))) by SIN_COS: 79

        .= ( - (((p . i) * ( sin r)) + ((p . j) * ( cos r))))

        .= ( - (Mp . j)) by A1, Th22

        .= s by A7;

      end;

    end;

    theorem :: MATRTOP3:26

    

     Th26: 1 <= i & i < j & j <= n implies ( Mx2Tran ( Rotation (i,j,n,r))) is {i, j} -support-yielding

    proof

      set M = ( Mx2Tran ( Rotation (i,j,n,r)));

      assume

       A1: 1 <= i & i < j & j <= n;

      let f be Function, x be set;

      assume that

       A2: f in ( dom M) and

       A3: ((M . f) . x) <> (f . x);

      reconsider p = f as Point of ( TOP-REAL n) by A2, FUNCT_2: 52;

      ( len p) = n by CARD_1:def 7;

      then

       A4: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

      ( len (M . p)) = n by CARD_1:def 7;

      then

       A5: ( dom (M . p)) = ( Seg n) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A6: not x in ( Seg n);

        then ((M . p) . x) = {} by A5, FUNCT_1:def 2;

        hence thesis by A3, A4, A6, FUNCT_1:def 2;

      end;

        suppose

         A7: x in ( Seg n);

        ((M . p) . x) <> (p . x) by A3;

        then x = i or x = j by A1, A7, Th20;

        hence thesis by TARSKI:def 2;

      end;

    end;

    begin

    definition

      let n;

      let f be Function of ( TOP-REAL n), ( TOP-REAL n);

      :: MATRTOP3:def4

      attr f is rotation means

      : Def4: |.p.| = |.(f . p).|;

    end

    theorem :: MATRTOP3:27

    

     Th27: i in ( Seg n) implies ( Mx2Tran ( AxialSymmetry (i,n))) is rotation

    proof

      set S = ( Seg n), M = ( Mx2Tran ( AxialSymmetry (i,n)));

      assume

       A1: i in S;

      let p be Point of ( TOP-REAL n);

      ( len p) = n by CARD_1:def 7;

      then

       A2: i in ( dom p) by A1, FINSEQ_1:def 3;

      

      thus |.(M . p).| = ( sqrt ( Sum ( sqr (p +* (i,( - (p . i))))))) by A1, Th10

      .= ( sqrt ((( Sum ( sqr p)) - ((p . i) ^2 )) + (( - (p . i)) ^2 ))) by A2, Th3

      .= |.p.|;

    end;

    definition

      let n;

      let f be Function of ( TOP-REAL n), ( TOP-REAL n);

      :: MATRTOP3:def5

      attr f is base_rotation means

      : Def5: ex F be FinSequence of ( GFuncs the carrier of ( TOP-REAL n)) st f = ( Product F) & for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)));

    end

    registration

      let n;

      cluster ( id ( TOP-REAL n)) -> base_rotation;

      coherence

      proof

        set S = the carrier of ( TOP-REAL n), G = ( GFuncs S);

        take F = ( <*> the carrier of G);

        

        thus ( Product F) = ( 1_ G) by GROUP_4: 8

        .= ( the_unity_wrt the multF of G) by GROUP_1: 22

        .= ( id ( TOP-REAL n)) by MONOID_0: 75;

        let k;

        assume k in ( dom F);

        hence thesis;

      end;

    end

    registration

      let n;

      cluster base_rotation for Function of ( TOP-REAL n), ( TOP-REAL n);

      existence

      proof

        ( id ( TOP-REAL n)) is base_rotation;

        hence thesis;

      end;

    end

    registration

      let n;

      let f,g be base_rotation Function of ( TOP-REAL n), ( TOP-REAL n);

      cluster (f * g) -> base_rotation;

      coherence

      proof

        consider F be FinSequence of ( GFuncs the carrier of ( TOP-REAL n)) such that

         A1: f = ( Product F) and

         A2: for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r))) by Def5;

        consider G be FinSequence of ( GFuncs the carrier of ( TOP-REAL n)) such that

         A3: g = ( Product G) and

         A4: for k st k in ( dom G) holds ex i, j, r st 1 <= i & i < j & j <= n & (G . k) = ( Mx2Tran ( Rotation (i,j,n,r))) by Def5;

        (f * g) is base_rotation

        proof

          take GF = (G ^ F);

          

          thus ( Product GF) = (( Product G) * ( Product F)) by GROUP_4: 5

          .= (f * g) by A3, A1, MONOID_0: 70;

          let k;

          assume

           A5: k in ( dom GF);

          per cases by A5, FINSEQ_1: 25;

            suppose

             A6: k in ( dom G);

            then (G . k) = (GF . k) by FINSEQ_1:def 7;

            hence thesis by A4, A6;

          end;

            suppose ex m st m in ( dom F) & k = (( len G) + m);

            then

            consider m such that

             A7: m in ( dom F) and

             A8: k = (( len G) + m);

            (GF . k) = (F . m) by A7, A8, FINSEQ_1:def 7;

            hence thesis by A2, A7;

          end;

        end;

        hence thesis;

      end;

    end

    

     Lm7: 1 <= i & i < j & j <= n implies ( Mx2Tran ( Rotation (i,j,n,r))) is rotation

    proof

      assume

       A1: 1 <= i & i < j & j <= n;

      let p;

      p = ( @ ( @ p));

      then

      reconsider P = p as FinSequence of REAL ;

      set M = ( Mx2Tran ( Rotation (i,j,n,r))), Mp = (M . p), p1 = (P | (i -' 1)), p2 = ((P /^ i) | ((j -' i) -' 1)), p3 = (P /^ j), s = ( sin r), c = ( cos r);

      reconsider pk = (P . i), pj = (P . j) as Element of REAL by XREAL_0:def 1;

      

       A2: ( sqr <*pk*>) = <*(pk ^2 )*> by RVSUM_1: 55;

      reconsider pij1 = ((pk * c) + (pj * ( - s))), pij2 = ((pk * s) + (pj * c)) as Element of REAL by XREAL_0:def 1;

      

       A3: ( sqr <*pij1*>) = <*(pij1 ^2 )*> by RVSUM_1: 55;

      

       A4: ( sqr <*pij2*>) = <*(pij2 ^2 )*> by RVSUM_1: 55;

      

       A5: ( sqr <*pj*>) = <*(pj ^2 )*> by RVSUM_1: 55;

      ( len p) = n by CARD_1:def 7;

      then p = ((((p1 ^ <*pk*>) ^ p2) ^ <*pj*>) ^ p3) by A1, FINSEQ_7: 1;

      

      then ( sqr p) = (( sqr (((p1 ^ <*pk*>) ^ p2) ^ <*pj*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= ((( sqr ((p1 ^ <*pk*>) ^ p2)) ^ ( sqr <*pj*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= (((( sqr (p1 ^ <*pk*>)) ^ ( sqr p2)) ^ ( sqr <*pj*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= ((((( sqr p1) ^ ( sqr <*pk*>)) ^ ( sqr p2)) ^ ( sqr <*pj*>)) ^ ( sqr p3)) by RVSUM_1: 144;

      

      then

       A6: ( Sum ( sqr p)) = (( Sum (((( sqr p1) ^ ( sqr <*pk*>)) ^ ( sqr p2)) ^ ( sqr <*pj*>))) + ( Sum ( sqr p3))) by RVSUM_1: 75

      .= ((( Sum ((( sqr p1) ^ ( sqr <*pk*>)) ^ ( sqr p2))) + (pj ^2 )) + ( Sum ( sqr p3))) by A5, RVSUM_1: 74

      .= (((( Sum (( sqr p1) ^ ( sqr <*pk*>))) + ( Sum ( sqr p2))) + (pj ^2 )) + ( Sum ( sqr p3))) by RVSUM_1: 75

      .= ((((( Sum ( sqr p1)) + (pk ^2 )) + ( Sum ( sqr p2))) + (pj ^2 )) + ( Sum ( sqr p3))) by A2, RVSUM_1: 74;

      

       A7: ((c * c) + (s * s)) = 1 by SIN_COS: 29;

      

       A8: ((pij1 ^2 ) + (pij2 ^2 )) = (((pk * pk) * ((c * c) + (s * s))) + ((pj * pj) * ((c * c) + (s * s))))

      .= ((pk ^2 ) + (pj ^2 )) by A7;

      Mp = ((((p1 ^ <*pij1*>) ^ p2) ^ <*pij2*>) ^ p3) by A1, Th23;

      

      then ( sqr Mp) = (( sqr (((p1 ^ <*pij1*>) ^ p2) ^ <*pij2*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= ((( sqr ((p1 ^ <*pij1*>) ^ p2)) ^ ( sqr <*pij2*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= (((( sqr (p1 ^ <*pij1*>)) ^ ( sqr p2)) ^ ( sqr <*pij2*>)) ^ ( sqr p3)) by RVSUM_1: 144

      .= ((((( sqr p1) ^ ( sqr <*pij1*>)) ^ ( sqr p2)) ^ ( sqr <*pij2*>)) ^ ( sqr p3)) by RVSUM_1: 144;

      

      then ( Sum ( sqr Mp)) = (( Sum (((( sqr p1) ^ ( sqr <*pij1*>)) ^ ( sqr p2)) ^ ( sqr <*pij2*>))) + ( Sum ( sqr p3))) by RVSUM_1: 75

      .= ((( Sum ((( sqr p1) ^ ( sqr <*pij1*>)) ^ ( sqr p2))) + (pij2 ^2 )) + ( Sum ( sqr p3))) by A4, RVSUM_1: 74

      .= (((( Sum (( sqr p1) ^ ( sqr <*pij1*>))) + ( Sum ( sqr p2))) + (pij2 ^2 )) + ( Sum ( sqr p3))) by RVSUM_1: 75

      .= ((((( Sum ( sqr p1)) + (pij1 ^2 )) + ( Sum ( sqr p2))) + (pij2 ^2 )) + ( Sum ( sqr p3))) by A3, RVSUM_1: 74;

      hence |.p.| = |.Mp.| by A6, A8;

    end;

    theorem :: MATRTOP3:28

    

     Th28: 1 <= i & i < j & j <= n implies ( Mx2Tran ( Rotation (i,j,n,r))) is base_rotation

    proof

      assume

       A1: 1 <= i & i < j & j <= n;

      set S = the carrier of ( TOP-REAL n), G = ( GFuncs S);

      reconsider M = ( Mx2Tran ( Rotation (i,j,n,r))) as Element of G by MONOID_0: 73;

      take F = <*M*>;

      thus ( Product F) = ( Mx2Tran ( Rotation (i,j,n,r))) by GROUP_4: 9;

      let k;

      assume k in ( dom F);

      then k in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then

       A2: k = 1 by TARSKI:def 1;

      (F . 1) = M by FINSEQ_1: 40;

      hence thesis by A1, A2;

    end;

    

     Lm8: for f,g be Function of ( TOP-REAL n), ( TOP-REAL n) st f is rotation & g is rotation holds (f * g) is rotation

    proof

      set TR = ( TOP-REAL n);

      let f,g be Function of TR, TR such that

       A1: f is rotation and

       A2: g is rotation;

      let p;

      ( dom (f * g)) = the carrier of TR by FUNCT_2: 52;

      

      hence |.((f * g) . p).| = |.(f . (g . p)).| by FUNCT_1: 12

      .= |.(g . p).| by A1

      .= |.p.| by A2;

    end;

    registration

      let n;

      cluster base_rotation -> homogeneous additive rotation being_homeomorphism for Function of ( TOP-REAL n), ( TOP-REAL n);

      coherence

      proof

        set TR = ( TOP-REAL n), G = ( GFuncs the carrier of TR);

        let f be Function of TR, TR;

        assume f is base_rotation;

        then

        consider F be FinSequence of G such that

         A1: f = ( Product F) and

         A2: for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)));

        defpred P[ Nat] means $1 <= ( len F) implies for g be Function of TR, TR st g = ( Product (F | $1)) holds g is homogeneous additive being_homeomorphism rotation;

        

         A3: for m st P[m] holds P[(m + 1)]

        proof

          let m;

          assume

           A4: P[m];

          set m1 = (m + 1);

          reconsider P = ( Product (F | m)) as Function of TR, TR by MONOID_0: 73;

          assume

           A5: m1 <= ( len F);

          1 <= m1 by NAT_1: 11;

          then

           A6: m1 in ( dom F) by A5, FINSEQ_3: 25;

          then

          consider i, j, r such that

           A7: 1 <= i & i < j & j <= n and

           A8: (F . m1) = ( Mx2Tran ( Rotation (i,j,n,r))) by A2;

          reconsider M = ( Mx2Tran ( Rotation (i,j,n,r))) as Element of G by MONOID_0: 73;

          

           A9: (F | m1) = ((F | m) ^ <*M*>) by A6, A8, FINSEQ_5: 10;

          let g be Function of TR, TR such that

           A10: g = ( Product (F | m1));

          

           A11: g = (( Product (F | m)) * M) by A9, A10, GROUP_4: 6

          .= (( Mx2Tran ( Rotation (i,j,n,r))) * P) by MONOID_0: 70;

          

           A12: ( Mx2Tran ( Rotation (i,j,n,r))) is rotation by A7, Lm7;

          P is homogeneous additive being_homeomorphism rotation by A4, A5, NAT_1: 13;

          hence thesis by A11, A12, Lm8, TOPS_2: 57;

        end;

        

         A13: (F | ( len F)) = F by FINSEQ_1: 58;

        

         A14: P[ 0 ]

        proof

          assume 0 <= ( len F);

          let g be Function of TR, TR;

          assume

           A15: g = ( Product (F | 0 ));

          (F | 0 ) = ( <*> the carrier of G);

          

          then g = ( 1_ G) by A15, GROUP_4: 8

          .= ( the_unity_wrt the multF of G) by GROUP_1: 22

          .= ( id TR) by MONOID_0: 75;

          hence thesis;

        end;

        for m holds P[m] from NAT_1:sch 2( A14, A3);

        hence thesis by A1, A13;

      end;

    end

    registration

      let n;

      let f be base_rotation Function of ( TOP-REAL n), ( TOP-REAL n);

      cluster (f " ) -> base_rotation;

      coherence

      proof

        set TR = ( TOP-REAL n), G = ( GFuncs the carrier of TR);

        defpred P[ Nat] means for F be FinSequence of G holds for f be Function of TR, TR st ( len F) = $1 & ( Product F) = f & (for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)))) holds (f " ) is base_rotation;

        consider F be FinSequence of G such that

         A1: f = ( Product F) & for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r))) by Def5;

        

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

        proof

          let z be Nat such that

           A3: P[z];

          set z1 = (z + 1);

          let F be FinSequence of G;

          let f be Function of TR, TR such that

           A4: ( len F) = z1 and

           A5: ( Product F) = f and

           A6: for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)));

          set Fz = (F | z);

          reconsider fz = ( Product Fz) as Function of TR, TR by MONOID_0: 73;

          1 <= z1 by NAT_1: 11;

          then z1 in ( dom F) by A4, FINSEQ_3: 25;

          then

          consider i, j, r such that

           A7: 1 <= i & i < j & j <= n and

           A8: (F . z1) = ( Mx2Tran ( Rotation (i,j,n,r))) by A6;

          set m = ( Mx2Tran ( Rotation (i,j,n,r)));

          reconsider M = m as Element of G by MONOID_0: 73;

          F = (Fz ^ <*M*>) by A4, A8, FINSEQ_3: 55;

          

          then

           A9: f = (( Product Fz) * M) by A5, GROUP_4: 6

          .= (m * fz) by MONOID_0: 70;

          

           A10: ( dom Fz) c= ( dom F) by RELAT_1: 60;

           A11:

          now

            let k;

            assume

             A12: k in ( dom Fz);

            then (Fz . k) = (F . k) by FUNCT_1: 47;

            hence ex i, j, r st 1 <= i & i < j & j <= n & (Fz . k) = ( Mx2Tran ( Rotation (i,j,n,r))) by A6, A10, A12;

          end;

          then

           A13: fz is base_rotation;

          ( Det ( Rotation (i,j,n,r))) <> ( 0. F_Real ) & (( Rotation (i,j,n,r)) ~ ) = ( Rotation (i,j,n,( - r))) by A7, Lm5, Th13;

          then

           A14: (m qua Function " ) = ( Mx2Tran ( Rotation (i,j,n,( - r)))) by MATRTOP1: 43;

          

           A15: ( rng m) = ( [#] TR) & m is one-to-one & ( dom m) = ( [#] TR) by TOPS_2:def 5;

          then m is onto by FUNCT_2:def 3;

          then

           A16: (m " ) = (m qua Function " ) by A15, TOPS_2:def 4;

          ( len Fz) = z by A4, FINSEQ_1: 59, NAT_1: 11;

          then

           A17: (fz " ) is base_rotation by A3, A11;

          (fz is one-to-one) & ( dom fz) = ( [#] TR) & ( rng fz) = ( [#] TR) by A13, TOPS_2:def 5;

          then

           A18: (f " ) = ((fz " ) * (m " )) by A9, A15, TOPS_2: 53;

          ( Mx2Tran ( Rotation (i,j,n,( - r)))) is base_rotation by A7, Th28;

          hence thesis by A14, A16, A17, A18;

        end;

        

         A19: P[ 0 ]

        proof

          let F be FinSequence of G;

          let f be Function of TR, TR;

          assume that

           A20: ( len F) = 0 and

           A21: ( Product F) = f;

          F = ( <*> the carrier of G) by A20;

          

          then

           A22: f = ( 1_ G) by A21, GROUP_4: 8

          .= ( the_unity_wrt the multF of G) by GROUP_1: 22

          .= ( id TR) by MONOID_0: 75;

          then ( rng f) = ( [#] TR);

          then f is onto by FUNCT_2:def 3;

          then (f /" ) = (f qua Function " ) by A22, TOPS_2:def 4;

          hence thesis by A22, FUNCT_1: 45;

        end;

        for i holds P[i] from NAT_1:sch 2( A19, A2);

        then P[( len F)];

        hence thesis by A1;

      end;

    end

    registration

      let n;

      let f,g be rotation Function of ( TOP-REAL n), ( TOP-REAL n);

      cluster (f * g) -> rotation;

      coherence by Lm8;

    end

    reserve f,f1,f2 for homogeneous additive Function of ( TOP-REAL n), ( TOP-REAL n);

    definition

      let n;

      let f;

      :: MATRTOP3:def6

      func AutMt f -> Matrix of n, F_Real means

      : Def6: f = ( Mx2Tran it );

      existence

      proof

        set T = (n -VectSp_over F_Real );

        set TR = ( TOP-REAL n);

        reconsider B = ( MX2FinS ( 1. ( F_Real ,n))) as OrdBasis of T by MATRLIN2: 45;

        

         A1: the carrier of T = ( REAL n) by MATRIX13: 102

        .= the carrier of TR by EUCLID: 22;

        then

        reconsider F = f as Function of T, T;

        now

          let v1,v2 be Vector of T;

          reconsider P1 = v1, P2 = v2, FP1 = (F . v1), FP2 = (F . v2) as Element of (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

          

           A2: ( @ ( @ FP1)) = FP1 & ( @ ( @ FP2)) = FP2;

          reconsider p1 = v1, p2 = v2 as Point of TR by A1;

          

           A3: ( @ ( @ P1)) = P1 & ( @ ( @ P2)) = P2;

          (v1 + v2) = (P1 + P2) by MATRIX13: 102

          .= (p1 + p2) by A3, MATRTOP1: 1;

          

          hence (F . (v1 + v2)) = ((f . p1) + (f . p2)) by VECTSP_1:def 20

          .= (FP1 + FP2) by A2, MATRTOP1: 1

          .= ((F . v1) + (F . v2)) by MATRIX13: 102;

        end;

        then

         A4: F is additive;

        ( len B) = n by MATRTOP1: 19;

        then

        reconsider A = ( AutMt (F,B,B)) as Matrix of n, F_Real ;

        take A;

        now

          let r be Scalar of F_Real , v be Vector of T;

          reconsider p = v as Point of TR by A1;

          reconsider P = v, FP = (F . v) as Element of (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

          (r * v) = (r * P) by MATRIX13: 102

          .= (r * p) by MATRIXR1: 17;

          

          hence (F . (r * v)) = (r * (f . p)) by TOPREAL9:def 4

          .= (r * FP) by MATRIXR1: 17

          .= (r * (F . v)) by MATRIX13: 102;

        end;

        then

         A5: F is homogeneous by MOD_2:def 2;

        ( Mx2Tran A) = ( Mx2Tran (( AutMt (F,B,B)),B,B)) by MATRTOP1: 20

        .= f by A5, A4, MATRLIN2: 34;

        hence thesis;

      end;

      uniqueness by MATRTOP1: 34;

    end

    theorem :: MATRTOP3:29

    

     Th29: ( AutMt (f1 * f2)) = (( AutMt f2) * ( AutMt f1))

    proof

      set A1 = ( AutMt f1), A2 = ( AutMt f2);

      

       A1: ( width A1) = n & ( width A2) = n & ( len A2) = n by MATRIX_0: 24;

      n = 0 implies n = 0 ;

      

      then ( Mx2Tran (A2 * A1)) = (( Mx2Tran A1) * ( Mx2Tran A2)) by A1, MATRTOP1: 32

      .= (f1 * ( Mx2Tran A2)) by Def6

      .= (f1 * f2) by Def6;

      hence thesis by Def6;

    end;

    theorem :: MATRTOP3:30

    

     Th30: k in X & k in ( Seg n) implies ex f st f is X -support-yielding base_rotation & (( card (X /\ ( Seg n))) > 1 implies ((f . p) . k) >= 0 ) & for i st i in (X /\ ( Seg n)) & i <> k holds ((f . p) . i) = 0

    proof

      assume that

       A1: k in X and

       A2: k in ( Seg n);

      set TR = ( TOP-REAL n);

      defpred P[ Nat] means $1 <= n implies ex f be base_rotation Function of TR, TR st f is ((X /\ ( Seg $1)) \/ {k}) -support-yielding & (( card ((X /\ ( Seg $1)) \/ {k})) > 1 implies ((f . p) . k) >= 0 ) & for i st i in (X /\ ( Seg $1)) & i <> k holds ((f . p) . i) = 0 ;

      

       A3: for z be Nat st P[z] holds P[(z + 1)]

      proof

        let z be Nat;

        set z1 = (z + 1);

        assume

         A4: P[z];

        

         A5: ( Seg z1) = (( Seg z) \/ {z1}) by FINSEQ_1: 9;

        

         A6: ( Seg z1) = (( Seg z) \/ {z1}) by FINSEQ_1: 9;

        

         A7: z1 in X implies (((X /\ ( Seg z)) \/ {k}) \/ {z1, k}) = ((X /\ ( Seg z1)) \/ {k})

        proof

          assume z1 in X;

          then

           A8: (X \/ {z1}) = X by ZFMISC_1: 40;

           {z1, k} = ( {z1} \/ {k}) by ENUMSET1: 1;

          

          hence (((X /\ ( Seg z)) \/ {k}) \/ {z1, k}) = ((X /\ ( Seg z)) \/ ( {k} \/ ( {k} \/ {z1}))) by XBOOLE_1: 4

          .= ((X /\ ( Seg z)) \/ (( {k} \/ {k}) \/ {z1})) by XBOOLE_1: 4

          .= (((X /\ ( Seg z)) \/ {z1}) \/ {k}) by XBOOLE_1: 4

          .= ((X /\ ( Seg z1)) \/ {k}) by A6, A8, XBOOLE_1: 24;

        end;

        assume

         A9: z1 <= n;

        then

        consider f be base_rotation Function of TR, TR such that

         A10: f is ((X /\ ( Seg z)) \/ {k}) -support-yielding and

         A11: ( card ((X /\ ( Seg z)) \/ {k})) > 1 implies ((f . p) . k) >= 0 and

         A12: for m st m in (X /\ ( Seg z)) & m <> k holds ((f . p) . m) = 0 by A4, NAT_1: 13;

        set z1 = (z + 1);

        per cases by XXREAL_0: 1;

          suppose

           A13: z1 = k;

          take f;

          (( Seg z1) \/ {z1}) = (( Seg z) \/ ( {z1} \/ {z1})) by A5, XBOOLE_1: 4

          .= (( Seg z) \/ {z1});

          

          then

           A14: ((X /\ ( Seg z1)) \/ {k}) = ((X \/ {k}) /\ (( Seg z) \/ {k})) by A13, XBOOLE_1: 24

          .= ((X /\ ( Seg z)) \/ {k}) by XBOOLE_1: 24;

          hence f is ((X /\ ( Seg z1)) \/ {k}) -support-yielding by A10;

          thus ( card ((X /\ ( Seg z1)) \/ {k})) > 1 implies ((f . p) . k) >= 0 by A11, A14;

          let m;

          assume that

           A15: m in (X /\ ( Seg z1)) and

           A16: m <> k;

          

           A17: m in ( Seg z1) by A15, XBOOLE_0:def 4;

          

           A18: m in X by A15, XBOOLE_0:def 4;

           not m in {z1} by A13, A16, TARSKI:def 1;

          then m in ( Seg z) by A5, A17, XBOOLE_0:def 3;

          then m in (X /\ ( Seg z)) by A18, XBOOLE_0:def 4;

          hence ((f . p) . m) = 0 by A12, A16;

        end;

          suppose

           A19: not z1 in X;

          take f;

          

           A20: {z1} misses X by A19, ZFMISC_1: 50;

          

           A21: (X /\ ( Seg z1)) = ((X /\ ( Seg z)) \/ (X /\ {z1})) by A5, XBOOLE_1: 23

          .= ((X /\ ( Seg z)) \/ {} ) by A20, XBOOLE_0:def 7

          .= (X /\ ( Seg z));

          hence f is ((X /\ ( Seg z1)) \/ {k}) -support-yielding by A10;

          thus ( card ((X /\ ( Seg z1)) \/ {k})) > 1 implies ((f . p) . k) >= 0 by A11, A21;

          let m;

          assume that

           A22: m in (X /\ ( Seg z1)) and

           A23: m <> k;

          

           A24: m in ( Seg z1) by A22, XBOOLE_0:def 4;

          

           A25: m in X by A22, XBOOLE_0:def 4;

          then not m in {z1} by A19, TARSKI:def 1;

          then m in ( Seg z) by A5, A24, XBOOLE_0:def 3;

          then m in (X /\ ( Seg z)) by A25, XBOOLE_0:def 4;

          hence ((f . p) . m) = 0 by A12, A23;

        end;

          suppose

           A26: z1 < k & z1 in X;

          set fp = (f . p);

          set S = (((fp . z1) ^2 ) + ((fp . k) ^2 ));

          

           A27: z1 >= 1 & k <= n by A2, FINSEQ_1: 1, NAT_1: 11;

          

           A28: ((fp . k) ^2 ) >= 0 & ((fp . z1) ^2 ) >= 0 by XREAL_1: 63;

          then

           A29: (( sqrt S) ^2 ) = S by SQUARE_1:def 2;

          then

          consider r such that

           A30: ((( Mx2Tran ( Rotation (z1,k,n,r))) . fp) . k) = ( sqrt S) by A26, A27, Th25;

          reconsider M = ( Mx2Tran ( Rotation (z1,k,n,r))) as base_rotation Function of TR, TR by A26, A27, Th28;

          take Mf = (M * f);

          

           A31: M is {z1, k} -support-yielding by A26, A27, Th26;

          hence Mf is ((X /\ ( Seg z1)) \/ {k}) -support-yielding by A7, A10, A26;

          

           A32: ( dom Mf) = the carrier of TR by FUNCT_2: 52;

          then

           A33: fp in ( dom M) by FUNCT_1: 11;

          

           A34: (Mf . p) = (M . fp) by A32, FUNCT_1: 12;

          hence ( card ((X /\ ( Seg z1)) \/ {k})) > 1 implies ((Mf . p) . k) >= 0 by A28, A30, SQUARE_1:def 2;

          let i;

          assume that

           A35: i in (X /\ ( Seg z1)) and

           A36: i <> k;

          

           A37: i in X by A35, XBOOLE_0:def 4;

          i in ( Seg z1) by A35, XBOOLE_0:def 4;

          then

           A38: i in ( Seg z) or i in {z1} by A5, XBOOLE_0:def 3;

          per cases by A38, TARSKI:def 1;

            suppose

             A39: i in ( Seg z);

            then

             A40: i in (X /\ ( Seg z)) by A37, XBOOLE_0:def 4;

            i <= z by A39, FINSEQ_1: 1;

            then i < z1 by NAT_1: 13;

            then not i in {z1, k} by A36, TARSKI:def 2;

            

            hence ((Mf . p) . i) = (fp . i) by A31, A33, A34

            .= 0 by A12, A36, A40;

          end;

            suppose i = z1;

            then

             A41: ((((M . fp) . i) * ((M . fp) . i)) + S) = S by A26, A27, A29, A30, Lm6;

            

            thus ((Mf . p) . i) = ((M . fp) . i) by A32, FUNCT_1: 12

            .= 0 by A41;

          end;

        end;

          suppose

           A42: z1 > k & z1 in X;

          set fp = (f . p);

          set S = (((fp . z1) ^2 ) + ((fp . k) ^2 ));

          

           A43: 1 <= k by A2, FINSEQ_1: 1;

          

           A44: ((fp . k) ^2 ) >= 0 & ((fp . z1) ^2 ) >= 0 by XREAL_1: 63;

          then

           A45: (( sqrt S) ^2 ) = S by SQUARE_1:def 2;

          then

          consider r such that

           A46: ((( Mx2Tran ( Rotation (k,z1,n,r))) . fp) . k) = ( sqrt S) by A9, A42, A43, Th24;

          reconsider M = ( Mx2Tran ( Rotation (k,z1,n,r))) as base_rotation Function of TR, TR by A9, A42, A43, Th28;

          take Mf = (M * f);

          

           A47: M is {k, z1} -support-yielding by A9, A42, A43, Th26;

          hence Mf is ((X /\ ( Seg z1)) \/ {k}) -support-yielding by A7, A10, A42;

          

           A48: ( dom Mf) = the carrier of TR by FUNCT_2: 52;

          then

           A49: (Mf . p) = (M . fp) by FUNCT_1: 12;

          hence ( card ((X /\ ( Seg z1)) \/ {k})) > 1 implies ((Mf . p) . k) >= 0 by A44, A46, SQUARE_1:def 2;

          let i;

          assume that

           A50: i in (X /\ ( Seg z1)) and

           A51: i <> k;

          

           A52: i in X by A50, XBOOLE_0:def 4;

          i in ( Seg z1) by A50, XBOOLE_0:def 4;

          then

           A53: i in ( Seg z) or i in {z1} by A5, XBOOLE_0:def 3;

          per cases by A53, TARSKI:def 1;

            suppose

             A54: i in ( Seg z);

            then i <= z by FINSEQ_1: 1;

            then i < z1 by NAT_1: 13;

            then

             A55: not i in {z1, k} by A51, TARSKI:def 2;

            

             A56: i in (X /\ ( Seg z)) by A52, A54, XBOOLE_0:def 4;

            fp in ( dom M) by A48, FUNCT_1: 11;

            

            hence ((Mf . p) . i) = (fp . i) by A47, A49, A55

            .= 0 by A12, A51, A56;

          end;

            suppose i = z1;

            then

             A57: ((((M . fp) . i) * ((M . fp) . i)) + S) = S by A9, A42, A43, A45, A46, Lm6;

            

            thus ((Mf . p) . i) = ((M . fp) . i) by A48, FUNCT_1: 12

            .= 0 by A57;

          end;

        end;

      end;

      

       A58: P[ 0 ]

      proof

        assume 0 <= n;

        take f = ( id TR);

        

         A59: f is {} -support-yielding by FUNCT_1: 17;

        thus f is ((X /\ ( Seg 0 )) \/ {k}) -support-yielding by A59;

        thus ( card ((X /\ ( Seg 0 )) \/ {k})) > 1 implies ((f . p) . k) >= 0 by CARD_2: 42;

        let m;

        assume m in (X /\ ( Seg 0 ));

        hence thesis;

      end;

      for z be Nat holds P[z] from NAT_1:sch 2( A58, A3);

      then

      consider f be base_rotation Function of TR, TR such that

       A60: (f is ((X /\ ( Seg n)) \/ {k}) -support-yielding) & (( card ((X /\ ( Seg n)) \/ {k})) > 1 implies ((f . p) . k) >= 0 ) & for i st i in (X /\ ( Seg n)) & i <> k holds ((f . p) . i) = 0 ;

      take f;

      

       A61: (X /\ ( Seg n)) c= X by XBOOLE_1: 17;

       {k} c= X & {k} c= ( Seg n) by A1, A2, ZFMISC_1: 31;

      then ((X /\ ( Seg n)) \/ {k}) = (X /\ ( Seg n)) by XBOOLE_1: 12, XBOOLE_1: 19;

      hence thesis by A60, A61;

    end;

    theorem :: MATRTOP3:31

    

     Th31: for A be Subset of ( TOP-REAL n) st (f | A) = ( id A) holds (f | ( Lin A)) = ( id ( Lin A))

    proof

      set TR = ( TOP-REAL n);

      let A be Subset of ( TOP-REAL n) such that

       A1: (f | A) = ( id A);

      defpred P[ Nat] means for L be Linear_Combination of A st ( card ( Carrier L)) <= $1 holds (f . ( Sum L)) = ( Sum L);

      

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

      proof

        let i;

        assume

         A3: P[i];

        set i1 = (i + 1);

        let L be Linear_Combination of A;

        assume

         A4: ( card ( Carrier L)) <= i1;

        per cases by A4, NAT_1: 8;

          suppose ( card ( Carrier L)) <= i;

          hence thesis by A3;

        end;

          suppose

           A5: ( card ( Carrier L)) = i1;

          then ( Carrier L) is non empty;

          then

          consider x be object such that

           A6: x in ( Carrier L) by XBOOLE_0:def 1;

          reconsider x as Point of TR by A6;

          reconsider X = {x} as Subset of TR by ZFMISC_1: 31;

          consider K be Linear_Combination of X such that

           A7: (K . x) = (L . x) by RLVECT_4: 37;

          (L . x) <> 0 by A6, RLVECT_2: 19;

          then ( Carrier K) c= {x} & x in ( Carrier K) by A7, RLVECT_2: 19, RLVECT_2:def 6;

          then

           A8: ( Carrier K) = {x} by ZFMISC_1: 33;

          ( {x} \/ ( Carrier L)) = ( Carrier L) by A6, ZFMISC_1: 40;

          then

           A9: ( Carrier (L - K)) c= ( Carrier L) by A8, RLVECT_2: 55;

          ((L - K) . x) = ((L . x) - (K . x)) by RLVECT_2: 54

          .= 0 by A7;

          then not x in ( Carrier (L - K)) by RLVECT_2: 19;

          then ( Carrier (L - K)) c< ( Carrier L) by A6, A9, XBOOLE_0:def 8;

          then ( card ( Carrier (L - K))) < i1 by A5, CARD_2: 48;

          then

           A10: ( card ( Carrier (L - K))) <= i by NAT_1: 13;

          ( ZeroLC TR) = (( - K) - ( - K)) by RLVECT_2: 57

          .= (( - K) + ( - ( - K))) by RLVECT_2:def 13

          .= (( - K) + K) by RLVECT_2: 53;

          

          then L = (L + (( - K) + K)) by RLVECT_2: 41

          .= ((L + ( - K)) + K) by RLVECT_2: 40

          .= ((L - K) + K) by RLVECT_2:def 13;

          then

           A11: ( Sum L) = (( Sum (L - K)) + ( Sum K)) by RLVECT_3: 1;

          

           A12: ( Carrier L) c= A by RLVECT_2:def 6;

          then ((f | A) . x) = (f . x) by A6, FUNCT_1: 49;

          then

           A13: (f . x) = x by A1, A6, A12, FUNCT_1: 17;

          ( Carrier (L - K)) c= A by A9, A12;

          then (L - K) is Linear_Combination of A by RLVECT_2:def 6;

          then

           A14: (f . ( Sum (L - K))) = ( Sum (L - K)) by A3, A10;

          ( Sum K) = ((L . x) * x) by A7, RLVECT_2: 32;

          then (f . ( Sum K)) = ( Sum K) by A13, TOPREAL9:def 4;

          hence (f . ( Sum L)) = ( Sum L) by A11, A14, VECTSP_1:def 20;

        end;

      end;

      set L = ( Lin A), cL = the carrier of L;

      cL c= the carrier of TR by RLSUB_1:def 2;

      then

       A15: (f | L) = (f | cL) by TMAP_1:def 3;

      

       A16: P[ 0 ]

      proof

        let L be Linear_Combination of A;

        assume ( card ( Carrier L)) <= 0 ;

        then ( Carrier L) = {} ;

        then L is Linear_Combination of ( {} the carrier of TR) by RLVECT_2:def 6;

        then

         A17: ( Sum L) = ( 0. TR) by RLVECT_2: 31;

        (f . ( 0. TR)) = (f . ( 0 qua Real * ( 0. TR))) by RLVECT_1: 10

        .= ( 0 qua Real * (f . ( 0. TR))) by TOPREAL9:def 4

        .= ( 0. TR) by RLVECT_1: 10;

        hence thesis by A17;

      end;

      

       A18: for i holds P[i] from NAT_1:sch 2( A16, A2);

      

       A19: for x be object st x in cL holds ((f | L) . x) = (( id L) . x)

      proof

        let x be object;

        assume

         A20: x in cL;

        then x in L;

        then

        consider K be Linear_Combination of A such that

         A21: ( Sum K) = x by RLVECT_3: 14;

         P[( card ( Carrier K))] by A18;

        then

         A22: (f . x) = x by A21;

        ((f | L) . x) = (f . x) by A15, A20, FUNCT_1: 49;

        hence thesis by A20, A22, FUNCT_1: 17;

      end;

      ( dom (f | L)) = cL & ( dom ( id L)) = cL by FUNCT_2:def 1;

      hence thesis by A19, FUNCT_1: 2;

    end;

    theorem :: MATRTOP3:32

    

     Th32: for A be Subset of ( TOP-REAL n) st f is rotation & (f | A) = ( id A) holds for i st i in ( Seg n) & ( Base_FinSeq (n,i)) in ( Lin A) holds ((f . p) . i) = (p . i)

    proof

      set TR = ( TOP-REAL n);

      let A be Subset of TR such that

       A1: f is rotation and

       A2: (f | A) = ( id A);

      set L = ( Lin A), n0 = ( 0* n);

      

       A3: (f | L) = ( id L) by A2, Th31;

      

       A4: ( len n0) = n by CARD_1:def 7;

      then

       A5: ( dom n0) = ( Seg n) by FINSEQ_1:def 3;

      let k such that

       A6: k in ( Seg n) and

       A7: ( Base_FinSeq (n,k)) in L;

      set n0k = (n0 +* (k,1));

      

       A8: n0k = ( Base_FinSeq (n,k)) by MATRIXR2:def 4;

      set pk = (p . k);

      the carrier of L c= the carrier of TR by RLSUB_1:def 2;

      then

       A9: (f | L) = (f | the carrier of L) by TMAP_1:def 3;

      ( dom n0k) = ( dom n0) by FUNCT_7: 30;

      then

       A10: ( len n0k) = n by A4, FINSEQ_3: 29;

      

       A11: n0k = ( @ ( @ n0k));

      then

      reconsider N0k = n0k as Point of TR by A10, TOPREAL3: 46;

      

       A12: n0k is Element of (n -tuples_on REAL ) by A10, A11, FINSEQ_2: 92;

      

       A13: for p st (p . k) <> 0 holds ((f . p) . k) = (p . k)

      proof

        let p;

        assume

         A14: (p . k) <> 0 ;

        set fp = (f . p), pk = (p . k);

        set pN = (pk * N0k);

        set ppN = (p - pN);

        

         A15: ((f . ppN) + (f . pN)) = (f . (ppN + pN)) by VECTSP_1:def 20;

        ( len (f . ppN)) = n & ( len (f . pN)) = n by CARD_1:def 7;

        then

         A16: ( |.(f . (ppN + pN)).| ^2 ) = ((( |.(f . ppN).| ^2 ) + (2 * |((f . pN), (f . ppN))|)) + ( |.(f . pN).| ^2 )) by A15, EUCLID_2: 11;

        

         A17: ((n |-> pk) . k) = pk by A6, FINSEQ_2: 57;

        

         A18: (pk * n0k) = ( mlt ((n |-> pk),n0k)) by A12, RVSUM_1: 63

        .= (( 0* n) +* (k,(pk * 1))) by A17, TOPREALC: 15

        .= (( 0* n) +* (k,pk));

        ( len fp) = n by CARD_1:def 7;

        then

         A19: ( dom fp) = ( Seg n) by FINSEQ_1:def 3;

        

         A20: ( len ppN) = n by CARD_1:def 7;

        then ( dom ppN) = ( Seg n) by FINSEQ_1:def 3;

        then

         A21: (ppN . k) = (pk - (pN . k)) by A6, VALUED_1: 13;

        ( len pN) = n by CARD_1:def 7;

        then

         A22: ( |.(ppN + pN).| ^2 ) = ((( |.ppN.| ^2 ) + (2 * |(pN, ppN)|)) + ( |.pN.| ^2 )) by A20, EUCLID_2: 11;

        pN in L by A7, A8, RLSUB_1: 21;

        then

         A23: pN in the carrier of L;

        

        then

         A24: pN = ((f | L) . pN) by A3, FUNCT_1: 17

        .= (f . pN) by A9, A23, FUNCT_1: 49;

         |.(ppN + pN).| = |.(f . (ppN + pN)).| & |.ppN.| = |.(f . ppN).| by A1;

        then |(pN, ppN)| = (pk * ((f . ppN) . k)) by A18, A16, A22, A24, TOPREALC: 16;

        then

         A25: (pk * (ppN . k)) = (pk * ((f . ppN) . k)) by A18, TOPREALC: 16;

        (pN . k) = pk by A6, A5, A18, FUNCT_7: 31;

        then

         A26: ((f . ppN) . k) = 0 by A14, A21, A25;

        (ppN + pN) = (p - (pN - pN)) by RLVECT_1: 29

        .= (p - ( 0. TR)) by RLVECT_1: 5

        .= p by RLVECT_1: 13;

        

        then (fp . k) = (((f . ppN) . k) + ((f . pN) . k)) by A6, A15, A19, VALUED_1:def 1

        .= (((f . ppN) . k) + pk) by A6, A5, A18, A24, FUNCT_7: 31;

        hence thesis by A26;

      end;

      per cases ;

        suppose (p . k) <> 0 ;

        hence thesis by A13;

      end;

        suppose (p . k) = 0 ;

        ( len (f . p)) = n by CARD_1:def 7;

        then

         A27: ( |.((f . p) + N0k).| ^2 ) = ((( |.(f . p).| ^2 ) + (2 * |(N0k, (f . p))|)) + ( |.N0k.| ^2 )) by A10, EUCLID_2: 11;

        ( len p) = n by CARD_1:def 7;

        then

         A28: ( |.(p + N0k).| ^2 ) = ((( |.p.| ^2 ) + (2 * |(N0k, p)|)) + ( |.N0k.| ^2 )) by A10, EUCLID_2: 11;

        

         A29: N0k in the carrier of L by A7, A8;

        

        then N0k = ((f | L) . N0k) by A3, FUNCT_1: 17

        .= (f . N0k) by A9, A29, FUNCT_1: 49;

        then

         A30: (f . (p + N0k)) = ((f . p) + N0k) by VECTSP_1:def 20;

         |.(p + N0k).| = |.(f . (p + N0k)).| & |.(f . p).| = |.p.| by A1;

        then |(N0k, (f . p))| = (1 * (p . k)) by A27, A28, A30, TOPREALC: 16;

        then (p . k) = (1 * ((f . p) . k)) by TOPREALC: 16;

        hence thesis;

      end;

    end;

    theorem :: MATRTOP3:33

    

     Th33: for f be rotation Function of ( TOP-REAL n), ( TOP-REAL n) st f is X -support-yielding & for i st i in (X /\ ( Seg n)) holds (p . i) = 0 holds (f . p) = p

    proof

      set TR = ( TOP-REAL n);

      let f be rotation Function of TR, TR such that

       A1: f is X -support-yielding and

       A2: for i st i in (X /\ ( Seg n)) holds (p . i) = 0 ;

      set sp = ( sqr p), sfp = ( sqr (f . p));

      

       A3: ( Sum sp) >= 0 by RVSUM_1: 86;

      ( Sum sfp) >= 0 & |.(f . p).| = |.p.| by Def4, RVSUM_1: 86;

      then

       A4: ( Sum sp) = ( Sum sfp) by A3, SQUARE_1: 28;

      

       A5: ( len p) = n by CARD_1:def 7;

      then

       A6: ( len sp) = n by RVSUM_1: 143;

      

       A7: ( len (f . p)) = n by CARD_1:def 7;

      then ( len sfp) = n by RVSUM_1: 143;

      then

      reconsider sp, sfp as Element of (n -tuples_on REAL ) by A6, FINSEQ_2: 92;

      

       A8: ( dom f) = the carrier of TR by FUNCT_2: 52;

      

       A9: for i st i in ( Seg n) holds (sp . i) <= (sfp . i)

      proof

        let i;

        

         A10: (sp . i) = ((p . i) ^2 ) & (sfp . i) = (((f . p) . i) ^2 ) by VALUED_1: 11;

        assume

         A11: i in ( Seg n);

        per cases ;

          suppose i in X;

          then i in (X /\ ( Seg n)) by A11, XBOOLE_0:def 4;

          then (p . i) = 0 by A2;

          hence thesis by A10, XREAL_1: 63;

        end;

          suppose not i in X;

          hence thesis by A1, A8, A10;

        end;

      end;

      for i st 1 <= i & i <= n holds (p . i) = ((f . p) . i)

      proof

        let i;

        

         A12: (sp . i) = ((p . i) ^2 ) by VALUED_1: 11;

        assume 1 <= i & i <= n;

        then

         A13: i in ( Seg n);

        then

         A14: (sp . i) >= (sfp . i) & (sp . i) <= (sfp . i) by A4, A9, RVSUM_1: 83;

        per cases ;

          suppose i in X;

          then

           A15: i in (X /\ ( Seg n)) by A13, XBOOLE_0:def 4;

          then (p . i) = 0 by A2;

          then (((f . p) . i) ^2 ) = 0 by A12, A14, VALUED_1: 11;

          then ((f . p) . i) = 0 ;

          hence thesis by A2, A15;

        end;

          suppose not i in X;

          hence thesis by A1, A8;

        end;

      end;

      hence thesis by A5, A7;

    end;

    theorem :: MATRTOP3:34

    

     Th34: i in ( Seg n) & n >= 2 implies ex f st f is base_rotation & (f . p) = (p +* (i,( - (p . i))))

    proof

      set TR = ( TOP-REAL n);

      assume that

       A1: i in ( Seg n) and

       A2: n >= 2;

      

       A3: {i} c= ( Seg n) by A1, ZFMISC_1: 31;

      

       A4: 1 <= i by A1, FINSEQ_1: 1;

      ( card ( Seg n)) = n & ( card {i}) = 1 by CARD_2: 42, FINSEQ_1: 57;

      then {i} <> ( Seg n) by A2;

      then {i} c< ( Seg n) by A3, XBOOLE_0:def 8;

      then

      consider j be object such that

       A5: j in ( Seg n) and

       A6: not j in {i} by XBOOLE_0: 6;

      reconsider j as Nat by A5;

      

       A7: j <> i by A6, TARSKI:def 1;

      

       A8: 1 <= j by A5, FINSEQ_1: 1;

      set p0 = (p +* (i,( - (p . i))));

      

       A9: ( len p0) = ( len p) by FUNCT_7: 97;

      

       A10: ( len p) = n by CARD_1:def 7;

      then

       A11: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

      

       A12: i <= n by A1, FINSEQ_1: 1;

      ((p . i) * (p . i)) >= 0 & ((p . j) * (p . j)) >= 0 by XREAL_1: 63;

      then

       A13: ( 0 ^2 ) = ( 0* 0 ) & 0 <= (((p . i) ^2 ) + ((p . j) ^2 ));

      

       A14: j <= n by A5, FINSEQ_1: 1;

      per cases by A7, XXREAL_0: 1;

        suppose

         A15: i < j;

        then

        consider r such that

         A16: ((( Mx2Tran ( Rotation (i,j,n,r))) . p) . i) = 0 by A4, A13, A14, Th24;

        set s = ( sin r), c = ( cos r);

        

         A17: 0 = (((p . i) * c) + ((p . j) * ( - s))) by A4, A14, A15, A16, Th21;

        reconsider M = ( Mx2Tran ( Rotation (i,j,n,(r + r)))) as base_rotation Function of TR, TR by A4, A14, A15, Th28;

        set Mp = (M . p);

        

         A18: ( cos (r + r)) = ((c * c) - (s * s)) & ( sin (r + r)) = ((s * c) + (s * c)) by SIN_COS: 75;

        

         A19: M is {i, j} -support-yielding by A4, A14, A15, Th26;

        

         A20: for k st 1 <= k & k <= n holds (p0 . k) = (Mp . k)

        proof

          let k;

          assume 1 <= k & k <= n;

          then

           A21: k in ( Seg n);

          per cases ;

            suppose

             A22: i = k;

            

            hence (p0 . k) = ( - ((p . i) * 1)) by A11, A21, FUNCT_7: 31

            .= ( - ((p . i) * ((s * s) + (c * c)))) by SIN_COS: 29

            .= ((((p . i) * ((c * c) - (s * s))) - (((p . i) * c) * c)) - (((p . i) * c) * c))

            .= ((((p . i) * ((c * c) - (s * s))) - (((p . j) * s) * c)) - (((p . j) * s) * c)) by A17

            .= (((p . i) * ((c * c) - (s * s))) + ((p . j) * ( - ((s * c) + (s * c)))))

            .= (Mp . k) by A4, A14, A15, A18, A22, Th21;

          end;

            suppose

             A23: j = k;

            

            hence (p0 . k) = ((p . j) * 1) by A15, FUNCT_7: 32

            .= ((p . j) * ((s * s) + (c * c))) by SIN_COS: 29

            .= (((((p . j) * s) * s) + (((p . j) * s) * s)) + ((p . j) * ((c * c) - (s * s))))

            .= (((((p . i) * c) * s) + (((p . i) * c) * s)) + ((p . j) * ((c * c) - (s * s)))) by A17

            .= (((p . i) * ((s * c) + (s * c))) + ((p . j) * ((c * c) - (s * s))))

            .= (Mp . k) by A4, A14, A15, A18, A23, Th22;

          end;

            suppose

             A24: i <> k & j <> k;

            

             A25: ( dom M) = the carrier of TR by FUNCT_2: 52;

            (p0 . k) = (p . k) & not k in {i, j} by A24, FUNCT_7: 32, TARSKI:def 2;

            hence thesis by A19, A25;

          end;

        end;

        take M;

        ( len Mp) = n by CARD_1:def 7;

        hence thesis by A9, A10, A20;

      end;

        suppose

         A26: j < i;

        then

        consider r such that

         A27: ((( Mx2Tran ( Rotation (j,i,n,r))) . p) . i) = 0 by A8, A12, A13, Th25;

        set s = ( sin r), c = ( cos r);

        

         A28: 0 = (((p . j) * s) + ((p . i) * c)) by A8, A12, A26, A27, Th22;

        reconsider M = ( Mx2Tran ( Rotation (j,i,n,(r + r)))) as base_rotation Function of TR, TR by A8, A12, A26, Th28;

        set Mp = (M . p);

        

         A29: ( cos (r + r)) = ((c * c) - (s * s)) & ( sin (r + r)) = ((s * c) + (s * c)) by SIN_COS: 75;

        

         A30: M is {i, j} -support-yielding by A8, A12, A26, Th26;

        

         A31: for k st 1 <= k & k <= n holds (p0 . k) = (Mp . k)

        proof

          let k;

          assume 1 <= k & k <= n;

          then

           A32: k in ( Seg n);

          per cases ;

            suppose

             A33: i = k;

            

            hence (p0 . k) = ( - ((p . i) * 1)) by A11, A32, FUNCT_7: 31

            .= ( - ((p . i) * ((s * s) + (c * c)))) by SIN_COS: 29

            .= ((( - (((p . i) * c) * c)) + (( - ((p . i) * c)) * c)) + ((p . i) * ((c * c) - (s * s))))

            .= (((((p . j) * s) * c) + (((p . j) * s) * c)) + ((p . i) * ((c * c) - (s * s)))) by A28

            .= (((p . j) * ((s * c) + (s * c))) + ((p . i) * ((c * c) - (s * s))))

            .= (Mp . k) by A8, A12, A26, A29, A33, Th22;

          end;

            suppose

             A34: j = k;

            

            hence (p0 . k) = ((p . j) * 1) by A26, FUNCT_7: 32

            .= ((p . j) * ((s * s) + (c * c))) by SIN_COS: 29

            .= ((((p . j) * ((c * c) - (s * s))) + (((p . j) * s) * s)) + (((p . j) * s) * s))

            .= ((((p . j) * ((c * c) - (s * s))) + (( - ((p . i) * c)) * s)) + (( - ((p . i) * c)) * s)) by A28

            .= (((p . j) * ((c * c) - (s * s))) + ((p . i) * ( - ((s * c) + (s * c)))))

            .= (Mp . k) by A8, A12, A26, A29, A34, Th21;

          end;

            suppose

             A35: i <> k & j <> k;

            

             A36: ( dom M) = the carrier of TR by FUNCT_2: 52;

            (p0 . k) = (p . k) & not k in {i, j} by A35, FUNCT_7: 32, TARSKI:def 2;

            hence thesis by A30, A36;

          end;

        end;

        take M;

        ( len Mp) = n by CARD_1:def 7;

        hence thesis by A9, A10, A31;

      end;

    end;

    

     Lm9: for f be homogeneous additive rotation Function of ( TOP-REAL n), ( TOP-REAL n) st f is X -support-yielding & not i in X holds (f . ( Base_FinSeq (n,i))) = ( Base_FinSeq (n,i))

    proof

      let f be homogeneous additive rotation Function of ( TOP-REAL n), ( TOP-REAL n);

      set B = ( Base_FinSeq (n,i));

      assume that

       A1: f is X -support-yielding and

       A2: not i in X;

       A3:

      now

        let j;

        assume

         A4: j in (X /\ ( Seg n));

        then j in ( Seg n) by XBOOLE_0:def 4;

        then

         A5: 1 <= j & j <= n by FINSEQ_1: 1;

        j <> i by A2, A4, XBOOLE_0:def 4;

        hence (B . j) = 0 by A5, MATRIXR2: 76;

      end;

      ( len B) = n by MATRIXR2: 74;

      then B is Point of ( TOP-REAL n) by TOPREAL3: 46;

      hence thesis by A1, A3, Th33;

    end;

    theorem :: MATRTOP3:35

    

     Th35: f is {i} -support-yielding rotation implies ( AutMt f) = ( AxialSymmetry (i,n)) or ( AutMt f) = ( 1. ( F_Real ,n))

    proof

      set TR = ( TOP-REAL n);

      set S = { ( Base_FinSeq (n,j)) where j be Element of NAT : 1 <= j & j <= n };

      S c= the carrier of TR

      proof

        let x be object;

        assume x in S;

        then

        consider j be Element of NAT such that

         A1: x = ( Base_FinSeq (n,j)) and 1 <= j & j <= n;

        ( len ( Base_FinSeq (n,j))) = n by MATRIXR2: 74;

        hence thesis by A1, TOPREAL3: 46;

      end;

      then

      reconsider S as Subset of TR;

      set M = ( Mx2Tran ( AxialSymmetry (n,i)));

      assume

       A2: f is {i} -support-yielding rotation;

      

       A3: ( id TR) = ( Mx2Tran ( 1. ( F_Real ,n))) by MATRTOP1: 33;

      then

       A4: ( AutMt ( id TR)) = ( 1. ( F_Real ,n)) by Def6;

      

       A5: ( dom f) = the carrier of TR by FUNCT_2: 52;

      per cases ;

        suppose

         A6: not i in ( Seg n);

        now

          let p be Point of TR;

           A7:

          now

            let j;

            assume 1 <= j & j <= n;

            then j <> i by A6;

            then not j in {i} by TARSKI:def 1;

            hence ((f . p) . j) = (p . j) by A2, A5;

          end;

          ( len (f . p)) = n & ( len p) = n by CARD_1:def 7;

          hence (f . p) = p by A7;

        end;

        then f = ( id TR) by FUNCT_2: 124;

        hence thesis by A3, Def6;

      end;

        suppose

         A8: i in ( Seg n);

        then 1 <= i & i <= n by FINSEQ_1: 1;

        then ( Base_FinSeq (n,i)) in S by A8;

        then

        reconsider B = ( Base_FinSeq (n,i)) as Point of TR;

        B = (( 0* n) +* (i,1)) by MATRIXR2:def 4;

        

        then

         A9: |.B.| = |.1.| by A8, TOPREALC: 13

        .= 1 by ABSVALUE:def 1;

        set B0 = (( 0* n) +* (i,((f . B) . i)));

        

         A10: ( len ( 0* n)) = n by CARD_1:def 7;

        

         A11: for j st 1 <= j & j <= n holds ((f . B) . j) = (B0 . j)

        proof

          let j;

          assume

           A12: 1 <= j & j <= n;

          

           A13: j in ( dom ( 0* n)) by A10, A12, FINSEQ_3: 25;

          per cases ;

            suppose j = i;

            hence (B0 . j) = ((f . B) . j) by A13, FUNCT_7: 31;

          end;

            suppose

             A14: j <> i;

            then

             A15: not j in {i} by TARSKI:def 1;

            

            thus (B0 . j) = (( 0* n) . j) by A14, FUNCT_7: 32

            .= 0

            .= (B . j) by A12, A14, MATRIXR2: 76

            .= ((f . B) . j) by A2, A5, A15;

          end;

        end;

        ( len B0) = ( len ( 0* n)) & ( len (f . B)) = n by CARD_1:def 7, FUNCT_7: 97;

        then

         A16: (f . B) = B0 by A10, A11;

        

        then

         A17: |.B.| = |.B0.| by A2

        .= |.((f . B) . i).| by A8, TOPREALC: 13;

        

         A18: for h be homogeneous additive rotation Function of TR, TR st (h | S) = ( id S) holds h = ( id TR)

        proof

          let h be homogeneous additive rotation Function of TR, TR;

          assume

           A19: (h | S) = ( id S);

          

           A20: for x be object st x in ( dom ( id TR)) holds (( id TR) . x) = (h . x)

          proof

            let x be object;

            assume x in ( dom ( id TR));

            then

            reconsider p = x as Point of TR;

            set hp = (h . p);

            

             A21: ( len p) = n & ( len hp) = n by CARD_1:def 7;

             A22:

            now

              let j;

              assume

               A23: 1 <= j & j <= n;

              then

               A24: j in ( Seg n);

              then ( Base_FinSeq (n,j)) in S by A23;

              then ( Base_FinSeq (n,j)) in ( Lin S) by RLVECT_3: 15;

              hence (p . j) = (hp . j) by A19, A24, Th32;

            end;

            thus thesis by A21, A22, FINSEQ_1: 14;

          end;

          ( dom h) = the carrier of TR by FUNCT_2:def 1;

          hence thesis by A20, FUNCT_1: 2;

        end;

        per cases ;

          suppose

           A25: ((f . B) . i) >= 0 ;

          

           A26: ( dom (f | S)) = S by A5, RELAT_1: 62;

          

           A27: ((f . B) . i) = 1 by A9, A17, A25, ABSVALUE:def 1;

          

           A28: for x be object st x in S holds ((f | S) . x) = (( id S) . x)

          proof

            let x be object;

            assume

             A29: x in S;

            then

            consider j be Element of NAT such that

             A30: x = ( Base_FinSeq (n,j)) and 1 <= j and j <= n;

            

             A31: ((f | S) . x) = (f . x) & (( id S) . x) = x by A26, A29, FUNCT_1: 17, FUNCT_1: 47;

            per cases ;

              suppose j = i;

              hence thesis by A16, A27, A30, A31, MATRIXR2:def 4;

            end;

              suppose j <> i;

              then not j in {i} by TARSKI:def 1;

              hence thesis by A2, A30, A31, Lm9;

            end;

          end;

          ( dom ( id S)) = S;

          hence thesis by A2, A4, A18, A26, A28, FUNCT_1: 2;

        end;

          suppose

           A32: ((f . B) . i) < 0 ;

          set MA = ( Mx2Tran ( AxialSymmetry (i,n)));

          MA is rotation by A8, Th27;

          then

          reconsider MAf = (MA * f) as homogeneous additive rotation Function of TR, TR by A2;

          

           A33: ( dom MAf) = the carrier of TR by FUNCT_2: 52;

          then

           A34: ( dom (MAf | S)) = S by RELAT_1: 62;

          

           A35: (MA is {i} -support-yielding) & ( {i} \/ {i}) = {i} by A8, Th11;

          

           A36: for x be object st x in S holds ((MAf | S) . x) = (( id S) . x)

          proof

            let x be object;

            assume

             A37: x in S;

            then

            consider j be Element of NAT such that

             A38: x = ( Base_FinSeq (n,j)) and 1 <= j & j <= n;

            

             A39: ((MAf | S) . x) = (MAf . x) & (( id S) . x) = x by A34, A37, FUNCT_1: 17, FUNCT_1: 47;

            per cases ;

              suppose

               A40: j = i;

              

               A41: for k st 1 <= k & k <= n holds ((MAf . B) . k) = (B . k)

              proof

                let k;

                assume

                 A42: 1 <= k & k <= n;

                then

                 A43: k in ( Seg n);

                per cases ;

                  suppose

                   A44: k = i;

                  

                  thus ((MAf . B) . k) = ((MA . (f . B)) . k) by A33, FUNCT_1: 12

                  .= ( - ((f . B) . k)) by A43, A44, Th9

                  .= ( - ( - 1)) by A9, A17, A32, A44, ABSVALUE:def 1

                  .= (B . k) by A42, A44, MATRIXR2: 75;

                end;

                  suppose

                   A45: k <> i;

                  then

                   A46: not k in {i} by TARSKI:def 1;

                  

                  thus ((MAf . B) . k) = ((MA . (f . B)) . k) by A33, FUNCT_1: 12

                  .= ((f . B) . k) by A8, A45, Th8

                  .= (B . k) by A2, A5, A46;

                end;

              end;

              ( len (MAf . B)) = n & ( len B) = n by CARD_1:def 7;

              hence thesis by A38, A39, A40, A41, FINSEQ_1: 14;

            end;

              suppose j <> i;

              then not j in {i} by TARSKI:def 1;

              hence thesis by A2, A35, A38, A39, Lm9;

            end;

          end;

          ( dom ( id S)) = S;

          then

           A47: MAf = ( id TR) by A18, A34, A36, FUNCT_1: 2;

          

           A48: ( dom MA) = ( [#] TR) by TOPS_2:def 5;

          set R = ( AutMt f);

          

           A49: ( rng MA) = ( [#] TR) by TOPS_2:def 5;

          

           A50: MA is one-to-one by TOPS_2:def 5;

          

           A51: the carrier of TR c= ( rng f)

          proof

            let x be object;

            assume

             A52: x in the carrier of TR;

            then

             A53: (MA . x) in ( rng MA) by A48, FUNCT_1:def 3;

            then

             A54: (MAf . (MA . x)) = (MA . (f . (MA . x))) by A33, A49, FUNCT_1: 12;

            (f . (MA . x)) in ( dom MA) & (MAf . (MA . x)) = (MA . x) by A33, A47, A49, A53, FUNCT_1: 11, FUNCT_1: 18;

            then x = (f . (MA . x)) by A48, A50, A52, A54, FUNCT_1:def 4;

            hence thesis by A5, A49, A53, FUNCT_1:def 3;

          end;

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

          then ( rng f) = the carrier of TR by A51, XBOOLE_0:def 10;

          then

           A55: f = (MA qua Function " ) by A47, A49, A48, A50, FUNCT_1: 42;

          ( Det ( AxialSymmetry (i,n))) = ( - ( 1. F_Real )) by A8, Th4;

          then f = ( Mx2Tran R) & ( Det ( AxialSymmetry (i,n))) <> ( 0. F_Real ) by Def6;

          

          then R = (( AxialSymmetry (i,n)) ~ ) by A55, MATRTOP1: 43

          .= ( AxialSymmetry (i,n)) by A8, Th7;

          hence thesis;

        end;

      end;

    end;

    theorem :: MATRTOP3:36

    

     Th36: f1 is rotation implies ex f2 st f2 is base_rotation & (f2 * f1) is {n} -support-yielding

    proof

      set TR = ( TOP-REAL n);

      assume

       A1: f1 is rotation;

      set cTR = the carrier of TR;

      set f = f1;

      

       A2: ( dom f) = cTR by FUNCT_2: 52;

      

       A3: ( rng f) c= cTR by RELAT_1:def 19;

      per cases ;

        suppose

         A4: n = 0 ;

        take I = ( id TR);

        

         A5: ( dom ( id cTR)) = cTR;

        

         A6: for h be Function, x be set st h in ( dom I) & ((I . h) . x) <> (h . x) holds x in {n} by FUNCT_1: 17;

        

         A7: cTR = {( 0. TR)} by A4, EUCLID: 22, EUCLID: 77;

        then ( rng ( id cTR)) = cTR & ( rng f) = cTR by A3, ZFMISC_1: 33;

        then f = ( id cTR) by A2, A5, A7, FUNCT_1: 7;

        then (I * f) = I by A2, RELAT_1: 52;

        hence thesis by A6;

      end;

        suppose n > 0 ;

        then

        reconsider n1 = (n - 1) as Nat;

        defpred P[ Nat] means $1 <= (n - 1) implies for S be Subset of TR st S = { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= $1 } holds ex g be base_rotation Function of TR, TR st ((g * f) | S) = ( id S);

        set S = { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= n1 };

        S c= the carrier of TR

        proof

          let x be object;

          assume x in S;

          then

          consider j be Element of NAT such that

           A8: x = ( Base_FinSeq (n,j)) and 1 <= j and j <= n1;

          ( len ( Base_FinSeq (n,j))) = n by MATRIXR2: 74;

          hence thesis by A8, TOPREAL3: 46;

        end;

        then

        reconsider S as Subset of TR;

        

         A9: for k st P[k] holds P[(k + 1)]

        proof

          let z be Nat;

          assume

           A10: P[z];

          set z1 = (z + 1);

          set SS = { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= z };

          assume

           A11: z1 <= (n - 1);

          then

          reconsider n1 = (n - 1) as Element of NAT by INT_1: 3;

          

           A12: n1 < (n1 + 1) by NAT_1: 13;

          then

           A13: z1 < n by A11, XXREAL_0: 2;

          set B = ( Base_FinSeq (n,z1));

          set X = { i where i be Element of NAT : z1 <= i & i <= n };

          let S be Subset of TR such that

           A14: S = { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= z1 };

          SS c= S

          proof

            let x be object;

            assume x in SS;

            then

            consider i be Element of NAT such that

             A15: x = ( Base_FinSeq (n,i)) & 1 <= i and

             A16: i <= z;

            i < z1 by A16, NAT_1: 13;

            hence thesis by A14, A15;

          end;

          then

          reconsider SS as Subset of TR by XBOOLE_1: 1;

          z < n1 by A11, NAT_1: 13;

          then

          consider g be base_rotation Function of TR, TR such that

           A17: ((g * f) | SS) = ( id SS) by A10;

          n in NAT by ORDINAL1:def 12;

          then

           A18: n in X by A13;

          n >= 1 by A12, NAT_1: 14;

          then n in ( Seg n);

          then

           A19: n in (X /\ ( Seg n)) by A18, XBOOLE_0:def 4;

          

           A20: ( card {z1, n}) = 2 by A11, A12, CARD_2: 57;

          

           A21: 1 <= z1 by NAT_1: 11;

          then

           A22: z1 in ( Seg n) by A13;

          B in S by A14, A21;

          then

          reconsider B as Point of TR;

          set gfB = ((g * f) . B);

          

           A23: z1 in X by A13;

          then

          consider h be homogeneous additive Function of TR, TR such that

           A24: h is X -support-yielding base_rotation and

           A25: ( card (X /\ ( Seg n))) > 1 implies ((h . gfB) . z1) >= 0 and

           A26: for i st i in (X /\ ( Seg n)) & i <> z1 holds ((h . gfB) . i) = 0 by A22, Th30;

          reconsider hg = (h * g) as base_rotation Function of TR, TR by A24;

          

           A27: ( dom (hg * f)) = the carrier of TR by FUNCT_2: 52;

          

           A28: for x st x in SS holds (((h * g) * f) . x) = x & (h . x) = x

          proof

            let x such that

             A29: x in SS;

            reconsider B = x as Point of TR by A29;

            (((g * f) | SS) . x) = ((g * f) . x) by A29, FUNCT_1: 49;

            then

             A30: ((g * f) . x) = x by A17, A29, FUNCT_1: 17;

            

             A31: ex i be Element of NAT st x = ( Base_FinSeq (n,i)) & 1 <= i & i <= z by A29;

            

             A32: for j st j in (X /\ ( Seg n)) holds (B . j) = 0

            proof

              let j;

              assume

               A33: j in (X /\ ( Seg n));

              then j in X by XBOOLE_0:def 4;

              then ex I be Element of NAT st I = j & z1 <= I & I <= n;

              then

               A34: z < j by NAT_1: 13;

              j in ( Seg n) by A33, XBOOLE_0:def 4;

              then 1 <= j & j <= n by FINSEQ_1: 1;

              hence thesis by A31, A34, MATRIXR2: 76;

            end;

            

             A35: (hg * f) = (h * (g * f)) by RELAT_1: 36;

            then ((h * (g * f)) . x) = (h . ((g * f) . x)) by A27, A29, FUNCT_1: 12;

            hence thesis by A24, A30, A32, A35, Th33;

          end;

          z1 in (X /\ ( Seg n)) by A22, A23, XBOOLE_0:def 4;

          then {z1, n} c= (X /\ ( Seg n)) by A19, ZFMISC_1: 32;

          then

           A36: (1 + 1) <= ( card (X /\ ( Seg n))) by A20, NAT_1: 43;

          

           A37: for x be object st x in S holds (((hg * f) | S) . x) = (( id S) . x)

          proof

            let x be object such that

             A38: x in S;

            

             A39: (( id S) . x) = x by A38, FUNCT_1: 17;

            

             A40: (hg * f) = (h * (g * f)) by RELAT_1: 36;

            

             A41: (((hg * f) | S) . x) = ((hg * f) . x) by A38, FUNCT_1: 49;

            consider i be Element of NAT such that

             A42: x = ( Base_FinSeq (n,i)) and

             A43: 1 <= i and

             A44: i <= z1 by A14, A38;

            per cases by A44, NAT_1: 8;

              suppose i <= z;

              then x in SS by A42, A43;

              hence thesis by A28, A39, A41;

            end;

              suppose

               A45: i = z1;

              set H = (h . gfB);

              

               A46: ((h * (g * f)) . x) = (h . gfB) by A27, A40, A42, A45, FUNCT_1: 12;

              

               A47: ( len H) = n by CARD_1:def 7;

              

               A48: for j st j in ( Seg n) & j < z1 holds ((h . gfB) . j) = 0

              proof

                let j;

                assume that

                 A49: j in ( Seg n) and

                 A50: j < z1;

                

                 A51: 1 <= j by A49, FINSEQ_1: 1;

                j <= z by A50, NAT_1: 13;

                then

                 A52: ( Base_FinSeq (n,j)) in SS by A49, A51;

                then

                reconsider Bnj = ( Base_FinSeq (n,j)) as Point of TR;

                (((h * g) * f) . Bnj) = Bnj by A28, A52;

                then

                 A53: (Bnj + H) = (((h * g) * f) . (Bnj + B)) by A40, A42, A45, A46, VECTSP_1:def 20;

                

                 A54: ( len Bnj) = n by CARD_1:def 7;

                 |.(((h * g) * f) . (Bnj + B)).| = |.(Bnj + B).| by A1, A24, Def4;

                then

                 A55: ( |.(Bnj + B).| ^2 ) = ((( |.Bnj.| ^2 ) + (2 * |(H, Bnj)|)) + ( |.H.| ^2 )) by A47, A53, A54, EUCLID_2: 11;

                

                 A56: Bnj = (( 0* n) +* (j,1)) by MATRIXR2:def 4;

                ( len B) = n by CARD_1:def 7;

                then

                 A57: ( |.(Bnj + B).| ^2 ) = ((( |.Bnj.| ^2 ) + (2 * |(B, Bnj)|)) + ( |.B.| ^2 )) by A54, EUCLID_2: 11;

                

                 A58: j <= n by A49, FINSEQ_1: 1;

                 |.H.| = |.B.| by A1, A24, A42, A45, A46, Def4;

                

                then ((B . j) * 1) = |(H, Bnj)| by A55, A56, A57, TOPREALC: 16

                .= ((H . j) * 1) by A56, TOPREALC: 16;

                hence thesis by A50, A51, A58, MATRIXR2: 76;

              end;

              set H = (h . gfB);

              set 0H = (( 0* n) +* (z1,(H . z1)));

              

               A59: ( len ( 0* n)) = n by CARD_1:def 7;

              

               A60: for j st j in ( Seg n) & j > z1 holds ((h . gfB) . j) = 0

              proof

                let j;

                assume that

                 A61: j in ( Seg n) and

                 A62: j > z1;

                j <= n by A61, FINSEQ_1: 1;

                then j in X by A61, A62;

                then j in (X /\ ( Seg n)) by A61, XBOOLE_0:def 4;

                hence thesis by A26, A62;

              end;

              

               A63: for j st 1 <= j & j <= n holds (H . j) = (0H . j)

              proof

                let j;

                assume 1 <= j & j <= n;

                then

                 A64: j in ( Seg n);

                then

                 A65: j in ( dom ( 0* n)) by A59, FINSEQ_1:def 3;

                per cases ;

                  suppose j = z1;

                  hence thesis by A65, FUNCT_7: 31;

                end;

                  suppose

                   A66: j <> z1;

                  then j > z1 or j < z1 by XXREAL_0: 1;

                  then

                   A67: (H . j) = 0 by A48, A60, A64;

                  (0H . j) = (( 0* n) . j) by A66, FUNCT_7: 32;

                  hence thesis by A67;

                end;

              end;

              ( len H) = n & ( len 0H) = ( len ( 0* n)) by CARD_1:def 7, FUNCT_7: 97;

              then

               A68: 0H = H by A59, A63;

              

               A69: |.gfB.| = |.B.| by A1, Def4;

              

               A70: B = (( 0* n) +* (z1,1)) by MATRIXR2:def 4;

              

              then

               A71: |.B.| = |.1.| by A22, TOPREALC: 13

              .= 1 by ABSVALUE:def 1;

               |.H.| = |.gfB.| & |.(H . z1).| = (H . z1) by A24, A25, A36, Def4, ABSVALUE:def 1, NAT_1: 13;

              then H = B by A22, A68, A70, A71, A69, TOPREALC: 13;

              hence thesis by A38, A39, A40, A42, A45, A46, FUNCT_1: 49;

            end;

          end;

          take hg;

          ( dom ( id S)) = S & ( dom ((hg * f) | S)) = S by A27, RELAT_1: 62;

          hence thesis by A37, FUNCT_1: 2;

        end;

        

         A72: P[ 0 ]

        proof

          assume 0 <= (n - 1);

          let S be Subset of TR such that

           A73: S = { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= 0 };

          

           A74: S = {}

          proof

            assume S <> {} ;

            then

            consider x be object such that

             A75: x in S by XBOOLE_0:def 1;

            ex i be Element of NAT st x = ( Base_FinSeq (n,i)) & 1 <= i & i <= 0 by A73, A75;

            hence contradiction;

          end;

          take g = ( id ( TOP-REAL n));

          ((g * f) | S) = {} by A74;

          hence thesis by A74;

        end;

        for k holds P[k] from NAT_1:sch 2( A72, A9);

        then

        consider g be base_rotation Function of TR, TR such that

         A76: ((g * f) | S) = ( id S);

        take g;

        set gf = (g * f);

        thus g is base_rotation;

        let p be Function;

        let x be set;

        assume that

         A77: p in ( dom gf) and

         A78: ((gf . p) . x) <> (p . x);

        reconsider p as Point of TR by A77, FUNCT_2: 52;

        ( len (gf . p)) = n by CARD_1:def 7;

        then ( dom (gf . p)) = ( Seg n) by FINSEQ_1:def 3;

        then

         A79: not x in ( Seg n) implies ((gf . p) . x) = {} by FUNCT_1:def 2;

        ( len p) = n by CARD_1:def 7;

        then ( dom p) = ( Seg n) by FINSEQ_1:def 3;

        then

         A80: x in ( Seg n) by A78, A79, FUNCT_1:def 2;

        assume

         A81: not x in {n};

        reconsider x as Nat by A80;

        

         A82: x <= n by A80, FINSEQ_1: 1;

        x <> n by A81, TARSKI:def 1;

        then x < (n1 + 1) by A82, XXREAL_0: 1;

        then

         A83: x <= n1 by NAT_1: 13;

        x in NAT & 1 <= x by A80, FINSEQ_1: 1;

        then ( Base_FinSeq (n,x)) in S by A83;

        then ( Base_FinSeq (n,x)) in ( Lin S) by RLVECT_3: 15;

        then ((gf . p) . x) = (p . x) by A1, A76, A80, Th32;

        hence contradiction by A78;

      end;

    end;

    

     Lm10: for M be Matrix of n, F_Real st ( Mx2Tran M) is base_rotation holds ( Det M) = ( 1. F_Real )

    proof

      let M be Matrix of n, F_Real ;

      set TR = ( TOP-REAL n), G = ( GFuncs the carrier of TR);

      assume ( Mx2Tran M) is base_rotation;

      then

      consider F be FinSequence of G such that

       A1: ( Mx2Tran M) = ( Product F) and

       A2: for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)));

      defpred P[ Nat] means $1 <= ( len F) implies ( Product (F | $1)) is base_rotation Function of TR, TR & for M be Matrix of n, F_Real st ( Mx2Tran M) = ( Product (F | $1)) holds ( Det M) = ( 1. F_Real );

      

       A3: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        

         A4: n = 0 implies n = 0 ;

        set m1 = (m + 1);

        assume

         A5: P[m];

        assume

         A6: m1 <= ( len F);

        then

        reconsider P = ( Product (F | m)) as base_rotation Function of TR, TR by A5, NAT_1: 13;

        set R = ( AutMt P);

        

         A7: ( width R) = n & ( len R) = n by MATRIX_0: 24;

        1 <= m1 by NAT_1: 11;

        then

         A8: m1 in ( dom F) by A6, FINSEQ_3: 25;

        then

        consider i, j, r such that

         A9: 1 <= i & i < j & j <= n and

         A10: (F . m1) = ( Mx2Tran ( Rotation (i,j,n,r))) by A2;

        set O = ( Rotation (i,j,n,r));

        reconsider MO = ( Mx2Tran O) as Element of G by MONOID_0: 73;

        (F | m1) = ((F | m) ^ <*MO*>) by A8, A10, FINSEQ_5: 10;

        

        then

         A11: ( Product (F | m1)) = (( Product (F | m)) * MO) by GROUP_4: 6

        .= (( Mx2Tran O) * P) by MONOID_0: 70;

        ( Mx2Tran O) is base_rotation by A9, Th28;

        hence ( Product (F | m1)) is base_rotation Function of TR, TR by A11;

        

         A12: ( width O) = n & ( len O) = n by MATRIX_0: 24;

        let M be Matrix of n, F_Real such that

         A13: ( Mx2Tran M) = ( Product (F | m1));

        ( Mx2Tran M) = (( Mx2Tran O) * ( Mx2Tran R)) by A11, A13, Def6

        .= ( Mx2Tran (R * O)) by A4, A12, A7, MATRTOP1: 32;

        then

         A14: M = (R * O) by MATRTOP1: 34;

        P = ( Mx2Tran R) by Def6;

        then

         A15: ( Det R) = ( 1. F_Real ) by A5, A6, NAT_1: 13;

        ( len R) = n & ( Det O) = ( 1. F_Real ) by A9, Th13, MATRIX_0: 25;

        

        hence ( Det M) = (( 1. F_Real ) * ( 1. F_Real )) by A14, A15, MATRIXR2: 45

        .= (( 1. F_Real ) * 1)

        .= ( 1. F_Real );

      end;

      

       A16: (F | ( len F)) = F by FINSEQ_1: 58;

      

       A17: P[ 0 ]

      proof

        assume 0 <= ( len F);

        

         A18: ( Mx2Tran ( 1. ( F_Real ,n))) = ( id TR) by MATRTOP1: 33;

        (F | 0 ) = ( <*> the carrier of G);

        

        then

         A19: ( Product (F | 0 )) = ( 1_ G) by GROUP_4: 8

        .= ( the_unity_wrt the multF of G) by GROUP_1: 22

        .= ( id TR) by MONOID_0: 75;

        hence ( Product (F | 0 )) is base_rotation Function of TR, TR;

        n = 0 or n >= 1 by NAT_1: 14;

        then

         A20: ( Det ( 1. ( F_Real ,n))) = ( 1_ F_Real ) & n >= 1 or ( Det ( 1. ( F_Real ,n))) = ( 1. F_Real ) & n = 0 by MATRIXR2: 41, MATRIX_7: 16;

        let M be Matrix of n, F_Real ;

        thus thesis by A18, A19, A20, MATRTOP1: 34;

      end;

      for m holds P[m] from NAT_1:sch 2( A17, A3);

      hence thesis by A1, A16;

    end;

    begin

    theorem :: MATRTOP3:37

    

     Th37: f is rotation implies (( Det ( AutMt f)) = ( 1. F_Real ) iff f is base_rotation)

    proof

      set TR = ( TOP-REAL n), cTR = the carrier of TR;

      set M = ( AutMt f);

      set MM = ( Mx2Tran M);

      

       A1: ( len M) = n & ( width M) = n by MATRIX_0: 24;

      

       A2: n = 0 implies n = 0 ;

      

       A3: MM = f by Def6;

      assume

       A4: f is rotation;

      then

      consider h be homogeneous additive Function of TR, TR such that

       A5: h is base_rotation and

       A6: (h * MM) is {n} -support-yielding by A3, Th36;

      set R = ( AutMt h);

      

       A7: ( width R) = n by MATRIX_0: 24;

      

       A8: h = ( Mx2Tran R) by Def6;

      

       A9: ( AutMt (h * MM)) = ( 1. ( F_Real ,n)) or ( AutMt (h * MM)) = ( AxialSymmetry (n,n)) by A4, A3, A5, A6, Th35;

      ( Det M) = ( 1. F_Real ) implies MM is base_rotation

      proof

        assume

         A10: ( Det M) = ( 1. F_Real );

        ( Det R) = ( 1. F_Real ) & n in NAT by A5, A8, Lm10, ORDINAL1:def 12;

        

        then

         A11: ( Det (M * R)) = (( 1. F_Real ) * ( 1. F_Real )) by A10, MATRIXR2: 45

        .= (1 * ( 1. F_Real ))

        .= ( 1. F_Real )

        .= 1;

        

         A12: ( rng MM) c= cTR by RELAT_1:def 19;

        

         A13: ( rng h) = ( [#] TR) by A5, TOPS_2:def 5;

        

         A14: ( dom h) = ( [#] TR) & h is one-to-one by A5, TOPS_2:def 5;

        

         A15: ( dom (h " )) = ( [#] TR) by A5, TOPS_2:def 5;

        

         A16: ( id TR) = ( Mx2Tran ( 1. ( F_Real ,n))) by MATRTOP1: 33;

        (h * MM) = ( id cTR)

        proof

          assume

           A17: (h * MM) <> ( id cTR);

          n <> 0

          proof

            

             A18: ( dom (h * MM)) = cTR & ( dom ( id cTR)) = cTR by FUNCT_2: 52;

            assume n = 0 ;

            then

             A19: cTR = {( 0. TR)} by EUCLID: 22, EUCLID: 77;

            ( rng (h * MM)) c= cTR by RELAT_1:def 19;

            then ( rng ( id cTR)) = cTR & ( rng (h * MM)) = cTR by A19, ZFMISC_1: 33;

            hence contradiction by A17, A18, A19, FUNCT_1: 7;

          end;

          then

           A20: n in ( Seg n) by FINSEQ_1: 3;

          ( Mx2Tran ( AutMt (h * MM))) = (h * MM) by Def6;

          then ( Mx2Tran ( AxialSymmetry (n,n))) = ( Mx2Tran (M * R)) by A1, A2, A9, A8, A7, A16, A17, MATRTOP1: 32;

          then ( AxialSymmetry (n,n)) = (M * R) by MATRTOP1: 34;

          then ( Det ( AxialSymmetry (n,n))) = ( Det (M * R));

          hence contradiction by A11, A20, Th4;

        end;

        then ((h " ) * (h * MM)) = (h " ) by A15, RELAT_1: 52;

        

        then (h " ) = (((h " ) * h) * MM) by RELAT_1: 36

        .= (( id cTR) * MM) by A14, A13, TOPS_2: 52

        .= MM by A12, RELAT_1: 53;

        hence thesis by A5;

      end;

      hence thesis by A3, Lm10;

    end;

    theorem :: MATRTOP3:38

    

     Th38: f is rotation implies (( Det ( AutMt f)) = ( 1. F_Real ) or ( Det ( AutMt f)) = ( - ( 1. F_Real )))

    proof

      set M = ( AutMt f);

      set MM = ( Mx2Tran M), TR = ( TOP-REAL n);

      

       A1: ( len M) = n & ( width M) = n by MATRIX_0: 24;

      

       A2: n = 0 implies n = 0 ;

      n = 0 or n >= 1 by NAT_1: 14;

      then

       A3: ( Det ( 1. ( F_Real ,n))) = ( 1_ F_Real ) & n >= 1 or ( Det ( 1. ( F_Real ,n))) = ( 1. F_Real ) & n = 0 by MATRIXR2: 41, MATRIX_7: 16;

      assume f is rotation;

      then

       A4: MM is rotation by Def6;

      then

      consider h be homogeneous additive Function of TR, TR such that

       A5: h is base_rotation and

       A6: (h * MM) is {n} -support-yielding by Th36;

      set R = ( AutMt h);

      

       A7: h = ( Mx2Tran R) by Def6;

      then n in NAT & ( Det R) = ( 1. F_Real ) by A5, Lm10, ORDINAL1:def 12;

      

      then

       A8: ( Det (M * R)) = (( Det M) * ( 1. F_Real )) by MATRIXR2: 45

      .= (( Det M) * 1)

      .= ( Det M);

      ( width R) = n by MATRIX_0: 24;

      then

       A9: (h * MM) = ( Mx2Tran (M * R)) by A1, A2, A7, MATRTOP1: 32;

      per cases by A4, A5, A6, Th35;

        suppose ( AutMt (h * MM)) = ( 1. ( F_Real ,n));

        hence thesis by A3, A8, A9, Def6;

      end;

        suppose

         A10: ( AutMt (h * MM)) <> ( 1. ( F_Real ,n)) & ( AutMt (h * MM)) = ( AxialSymmetry (n,n));

        set cTR = the carrier of TR;

        n <> 0

        proof

          

           A11: ( dom (h * MM)) = cTR & ( dom ( id cTR)) = cTR by FUNCT_2: 52;

          assume n = 0 ;

          then

           A12: cTR = {( 0. TR)} by EUCLID: 22, EUCLID: 77;

          ( rng (h * MM)) c= cTR by RELAT_1:def 19;

          then ( rng ( id cTR)) = cTR & ( rng (h * MM)) = cTR by A12, ZFMISC_1: 33;

          

          then (h * MM) = ( id TR) by A11, A12, FUNCT_1: 7

          .= ( Mx2Tran ( 1. ( F_Real ,n))) by MATRTOP1: 33;

          hence contradiction by A10, Def6;

        end;

        then n in ( Seg n) by FINSEQ_1: 3;

        then ( Det ( AxialSymmetry (n,n))) = ( - ( 1. F_Real )) by Th4;

        hence thesis by A8, A9, A10, Def6;

      end;

    end;

    theorem :: MATRTOP3:39

    

     Th39: f1 is rotation & ( Det ( AutMt f1)) = ( - ( 1. F_Real )) & i in ( Seg n) & ( AutMt f2) = ( AxialSymmetry (i,n)) implies (f1 * f2) is base_rotation

    proof

      set M = ( AutMt f1);

      set A = ( AutMt f2);

      assume that

       A1: f1 is rotation and

       A2: ( Det M) = ( - ( 1. F_Real )) and

       A3: i in ( Seg n) and

       A4: A = ( AxialSymmetry (i,n));

      

       A5: f2 = ( Mx2Tran ( AxialSymmetry (i,n))) by A4, Def6;

      reconsider MF = (( Mx2Tran M) * f2) as homogeneous additive Function of ( TOP-REAL n), ( TOP-REAL n);

      set A = ( AxialSymmetry (i,n));

      set R = ( AutMt MF);

      

       A6: n = 0 implies n = 0 ;

      

       A7: MF = ( Mx2Tran R) & ( width M) = n by Def6, MATRIX_0: 24;

      ( len A) = n & ( width A) = n by MATRIX_0: 24;

      then ( Mx2Tran R) = ( Mx2Tran (A * M)) by A5, A6, A7, MATRTOP1: 32;

      then

       A8: R = (A * M) by MATRTOP1: 34;

      n in NAT & ( Det A) = ( - ( 1. F_Real )) by A3, Th4, ORDINAL1:def 12;

      

      then

       A9: ( Det R) = (( - ( 1. F_Real )) * ( - ( 1. F_Real ))) by A2, A8, MATRIXR2: 45

      .= (( - ( 1. F_Real )) * ( - 1))

      .= ( 1. F_Real );

      

       A10: ( Mx2Tran M) = f1 by Def6;

      f2 is rotation by A3, A5, Th27;

      hence thesis by A10, A1, A9, Th37;

    end;

    

     Lm11: f is base_rotation implies ( AutMt f) is Orthogonal

    proof

      set TR = ( TOP-REAL n), G = ( GFuncs the carrier of TR);

      assume f is base_rotation;

      then

      consider F be FinSequence of G such that

       A1: f = ( Product F) and

       A2: for k st k in ( dom F) holds ex i, j, r st 1 <= i & i < j & j <= n & (F . k) = ( Mx2Tran ( Rotation (i,j,n,r)));

      

       A3: f = ( Mx2Tran ( AutMt f)) by Def6;

      defpred P[ Nat] means $1 <= ( len F) implies ( Product (F | $1)) is base_rotation Function of TR, TR & for M be Matrix of n, F_Real st ( Mx2Tran M) = ( Product (F | $1)) holds M is Orthogonal;

      

       A4: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        

         A5: n = 0 implies n = 0 ;

        set m1 = (m + 1);

        assume

         A6: P[m];

        assume

         A7: m1 <= ( len F);

        then

        reconsider P = ( Product (F | m)) as base_rotation Function of TR, TR by A6, NAT_1: 13;

        set R = ( AutMt P);

        

         A8: ( width R) = n & ( len R) = n by MATRIX_0: 24;

        1 <= m1 by NAT_1: 11;

        then

         A9: m1 in ( dom F) by A7, FINSEQ_3: 25;

        then

        consider i, j, r such that

         A10: 1 <= i & i < j & j <= n and

         A11: (F . m1) = ( Mx2Tran ( Rotation (i,j,n,r))) by A2;

        set O = ( Rotation (i,j,n,r));

        reconsider MO = ( Mx2Tran O) as Element of G by MONOID_0: 73;

        (F | m1) = ((F | m) ^ <*MO*>) by A9, A11, FINSEQ_5: 10;

        

        then

         A12: ( Product (F | m1)) = (( Product (F | m)) * MO) by GROUP_4: 6

        .= (( Mx2Tran O) * P) by MONOID_0: 70;

        ( Mx2Tran O) is base_rotation by A10, Th28;

        hence ( Product (F | m1)) is base_rotation Function of TR, TR by A12;

        

         A13: ( width O) = n & ( len O) = n by MATRIX_0: 24;

        let M be Matrix of n, F_Real such that

         A14: ( Mx2Tran M) = ( Product (F | m1));

        ( Mx2Tran M) = (( Mx2Tran O) * ( Mx2Tran R)) by A12, A14, Def6

        .= ( Mx2Tran (R * O)) by A5, A13, A8, MATRTOP1: 32;

        then

         A15: M = (R * O) by MATRTOP1: 34;

        P = ( Mx2Tran R) by Def6;

        then

         A16: R is Orthogonal & n > i by A10, A6, A7, NAT_1: 13, XXREAL_0: 2;

        ( len R) = n & O is Orthogonal & n > 0 by A10, Th19, MATRIX_0: 25;

        hence M is Orthogonal by A15, A16, MATRIX_6: 46;

      end;

      

       A17: (F | ( len F)) = F by FINSEQ_1: 58;

      

       A18: P[ 0 ]

      proof

        assume 0 <= ( len F);

        

         A19: ( Mx2Tran ( 1. ( F_Real ,n))) = ( id TR) by MATRTOP1: 33;

        (F | 0 ) = ( <*> the carrier of G);

        

        then

         A20: ( Product (F | 0 )) = ( 1_ G) by GROUP_4: 8

        .= ( the_unity_wrt the multF of G) by GROUP_1: 22

        .= ( id TR) by MONOID_0: 75;

        hence ( Product (F | 0 )) is base_rotation Function of TR, TR;

        

         A21: ( 1. ( F_Real ,n)) is Orthogonal by MATRIX_6: 58;

        let M be Matrix of n, F_Real ;

        thus thesis by A19, A20, A21, MATRTOP1: 34;

      end;

      for m holds P[m] from NAT_1:sch 2( A18, A4);

      hence thesis by A1, A17, A3;

    end;

    registration

      let n;

      let f be rotation homogeneous additive Function of ( TOP-REAL n), ( TOP-REAL n);

      cluster ( AutMt f) -> Orthogonal;

      coherence

      proof

        set TR = ( TOP-REAL n), cTR = the carrier of TR, M = ( AutMt f);

        per cases by Th37, Th38;

          suppose ( Det M) = ( 1. F_Real );

          then f is base_rotation by Th37;

          hence thesis by Lm11;

        end;

          suppose

           A1: ( Det M) = ( - ( 1. F_Real )) & not f is base_rotation;

          

           A2: n > 0

          proof

            

             A3: ( dom f) = cTR & ( dom ( id cTR)) = cTR by FUNCT_2: 52;

            assume n <= 0 ;

            then n = 0 ;

            then

             A4: cTR = {( 0. TR)} by EUCLID: 22, EUCLID: 77;

            ( rng f) c= cTR by RELAT_1:def 19;

            then ( rng ( id cTR)) = cTR & ( rng f) = cTR by A4, ZFMISC_1: 33;

            then f = ( id TR) by A3, A4, FUNCT_1: 7;

            hence contradiction by A1;

          end;

          then

           A5: n in ( Seg n) by FINSEQ_1: 3;

          set A = ( AxialSymmetry (n,n)), MA = ( Mx2Tran A);

          ( AutMt MA) = A by Def6;

          then

           A6: (f * MA) is base_rotation by A1, A5, Th39;

          A is diagonal & (A ~ ) = A by A5, Th7;

          then (A @ ) = (A ~ ) by Th2;

          then

           A7: A is Orthogonal & ( AutMt (f * MA)) is Orthogonal by A6, Lm11, MATRIX_6:def 7;

          

           A8: ( AutMt (f * MA)) = (( AutMt MA) * M) by Th29

          .= (A * M) by Def6;

          (A ~ ) is_reverse_of A by MATRIX_6:def 4;

          then

           A9: ((A ~ ) * A) = ( 1. ( F_Real ,n)) by MATRIX_6:def 2;

          ( width (A ~ )) = n & ( len A) = n & ( width A) = n & ( len M) = n by MATRIX_0: 24;

          

          then ((A ~ ) * (A * M)) = (((A ~ ) * A) * M) by MATRIX_3: 33

          .= M by A9, MATRIX_3: 18;

          hence thesis by A2, A7, A8, MATRIX_6: 59;

        end;

      end;

    end

    registration

      let n;

      cluster homogeneous additive rotation -> being_homeomorphism for Function of ( TOP-REAL n), ( TOP-REAL n);

      coherence

      proof

        set TR = ( TOP-REAL n), cTR = the carrier of TR;

        let f be Function of TR, TR;

        assume

         A1: f is homogeneous additive rotation;

        then

        reconsider F = f as homogeneous additive Function of TR, TR;

        set M = ( AutMt F);

        per cases by A1, Th37, Th38;

          suppose ( Det M) = ( 1. F_Real );

          then f is base_rotation by A1, Th37;

          hence thesis;

        end;

          suppose

           A2: ( Det M) = ( - ( 1. F_Real )) & not f is base_rotation;

          n <> 0

          proof

            

             A3: ( dom f) = cTR & ( dom ( id cTR)) = cTR by FUNCT_2: 52;

            assume n = 0 ;

            then

             A4: cTR = {( 0. TR)} by EUCLID: 22, EUCLID: 77;

            ( rng f) c= cTR by RELAT_1:def 19;

            then ( rng ( id cTR)) = cTR & ( rng f) = cTR by A4, ZFMISC_1: 33;

            then f = ( id TR) by A3, A4, FUNCT_1: 7;

            hence contradiction by A2;

          end;

          then

           A5: n in ( Seg n) by FINSEQ_1: 3;

          

           A6: ( dom f) = cTR by FUNCT_2: 52;

          set A = ( AxialSymmetry (n,n)), MA = ( Mx2Tran A);

          

           A7: (MA " ) is being_homeomorphism by TOPS_2: 56;

          

           A8: (MA is one-to-one) & ( rng MA) = ( [#] TR) by TOPS_2:def 5;

          ( AutMt MA) = A by Def6;

          then

           A9: (f * MA) is base_rotation by A1, A2, A5, Th39;

          ((f * MA) * (MA " )) = (f * (MA * (MA " ))) by RELAT_1: 36

          .= (f * ( id cTR)) by A8, TOPS_2: 52

          .= f by A6, RELAT_1: 51;

          hence thesis by A9, A7, TOPS_2: 57;

        end;

      end;

    end

    begin

    theorem :: MATRTOP3:40

    n = 1 & |.p.| = |.q.| implies ex f st f is rotation & (f . p) = q & (( AutMt f) = ( AxialSymmetry (n,n)) or ( AutMt f) = ( 1. ( F_Real ,n)))

    proof

      set TR = ( TOP-REAL n);

      assume that

       A1: n = 1 and

       A2: |.p.| = |.q.|;

      per cases ;

        suppose

         A3: p = q;

        take I = ( id TR);

        ( id TR) = ( Mx2Tran ( 1. ( F_Real ,1))) by A1, MATRTOP1: 33;

        hence thesis by A1, A3, Def6;

      end;

        suppose

         A4: p <> q;

        

         A5: ( len p) = 1 by A1, CARD_1:def 7;

        then

         A6: p = <*(p . 1)*> by FINSEQ_1: 40;

        

         A7: 1 in ( Seg 1);

        then

        reconsider f = ( Mx2Tran ( AxialSymmetry (1,1))) as homogeneous additive rotation Function of TR, TR by A1, Th27;

        take f;

        

         A8: ((q . 1) ^2 ) >= 0 & ((p . 1) ^2 ) >= 0 by XREAL_1: 63;

        reconsider pk = ((p . 1) ^2 ), qk = ((q . 1) ^2 ) as Real;

        

         A9: |.p.| = ( sqrt ( Sum ( sqr <*(p . 1)*>))) by A5, FINSEQ_1: 40

        .= ( sqrt ( Sum <*pk*>)) by RVSUM_1: 55

        .= ( sqrt ((p . 1) ^2 )) by RVSUM_1: 73;

        

         A10: ( len q) = 1 by A1, CARD_1:def 7;

        then

         A11: q = <*(q . 1)*> by FINSEQ_1: 40;

         |.q.| = ( sqrt ( Sum ( sqr <*(q . 1)*>))) by A10, FINSEQ_1: 40

        .= ( sqrt ( Sum <*qk*>)) by RVSUM_1: 55

        .= ( sqrt ((q . 1) ^2 )) by RVSUM_1: 73;

        then

         A12: ((q . 1) ^2 ) = ((p . 1) ^2 ) by A2, A8, A9, SQUARE_1: 28;

        ( len (f . p)) = 1 by A1, CARD_1:def 7;

        

        then (f . p) = <*((f . p) . 1)*> by FINSEQ_1: 40

        .= <*( - (p . 1))*> by A1, A7, Th9

        .= q by A4, A6, A11, A12, SQUARE_1: 40;

        hence thesis by A1, Def6;

      end;

    end;

    theorem :: MATRTOP3:41

    n <> 1 & |.p.| = |.q.| implies ex f st f is base_rotation & (f . p) = q

    proof

      set TR = ( TOP-REAL n);

      assume

       A1: n <> 1;

      assume

       A2: |.p.| = |.q.|;

      per cases ;

        suppose

         A3: p = q;

        take I = ( id TR);

        thus thesis by A3;

      end;

        suppose

         A4: p <> q;

        

         A5: n <> 0

        proof

          assume

           A6: n = 0 ;

          then p = ( 0. TR) by EUCLID: 77;

          hence thesis by A4, A6;

        end;

        then

         A7: n >= 1 by NAT_1: 14;

        defpred P[ Nat] means ($1 + 1) <= n implies ex f be base_rotation Function of TR, TR, X be set st ( card X) = $1 & X c= ( Seg n) & for k st k in X holds ((f . p) . k) = (q . k);

        

         A8: ( Sum ( sqr q)) >= 0 by RVSUM_1: 86;

        

         A9: ( card ( Seg n)) = n by FINSEQ_1: 57;

        

         A10: for m st P[m] holds P[(m + 1)]

        proof

          let m such that

           A11: P[m];

          set m1 = (m + 1);

          assume

           A12: (m1 + 1) <= n;

          then

          consider f be base_rotation Function of TR, TR, Xm be set such that

           A13: ( card Xm) = m and

           A14: Xm c= ( Seg n) and

           A15: for k st k in Xm holds ((f . p) . k) = (q . k) by A11, NAT_1: 13;

          set fp = (f . p), sfp = ( sqr fp), sq = ( sqr q);

          

           A16: m1 < n by A12, NAT_1: 13;

          per cases ;

            suppose ex k st k in (( Seg n) \ Xm) & (sfp . k) >= (sq . k);

            then

            consider k such that

             A17: k in (( Seg n) \ Xm) and

             A18: (sfp . k) >= (sq . k);

            

             A19: k in ( Seg n) by A17, XBOOLE_0:def 5;

            then

             A20: 1 <= k by FINSEQ_1: 1;

            set Xmk = (Xm \/ {k});

            

             A21: (sfp . k) = ((fp . k) ^2 ) & (sq . k) = ((q . k) ^2 ) by VALUED_1: 11;

            

             A22: {k} c= ( Seg n) by A19, ZFMISC_1: 31;

            then

             A23: Xmk c= ( Seg n) by A14, XBOOLE_1: 8;

            

             A24: not k in Xm by A17, XBOOLE_0:def 5;

            then ( card Xmk) = m1 by A13, A14, CARD_2: 41;

            then Xmk c< ( Seg n) by A9, A16, A23, XBOOLE_0:def 8;

            then

            consider z be object such that

             A25: z in ( Seg n) and

             A26: not z in Xmk by XBOOLE_0: 6;

            reconsider z as Nat by A25;

            

             A27: 1 <= z by A25, FINSEQ_1: 1;

            ((fp . z) ^2 ) >= 0 by XREAL_1: 63;

            then

             A28: ( 0 + ((q . k) ^2 )) <= (((fp . z) ^2 ) + ((fp . k) ^2 )) by A18, A21, XREAL_1: 7;

            

             A29: z <= n by A25, FINSEQ_1: 1;

            

             A30: k <= n by A19, FINSEQ_1: 1;

             not z in {k} by A26, XBOOLE_0:def 3;

            then

             A31: z <> k by TARSKI:def 1;

            now

              per cases by A31, XXREAL_0: 1;

                suppose

                 A32: z < k;

                then

                consider r such that

                 A33: ((( Mx2Tran ( Rotation (z,k,n,r))) . fp) . k) = (q . k) by A27, A28, A30, Th25;

                ( Mx2Tran ( Rotation (z,k,n,r))) is {k, z} -support-yielding base_rotation by A27, A30, A32, Th28, Th26;

                hence ex g be base_rotation Function of TR, TR st g is {k, z} -support-yielding & ((g . fp) . k) = (q . k) by A33;

              end;

                suppose

                 A34: z > k;

                then

                consider r such that

                 A35: ((( Mx2Tran ( Rotation (k,z,n,r))) . fp) . k) = (q . k) by A20, A28, A29, Th24;

                ( Mx2Tran ( Rotation (k,z,n,r))) is {z, k} -support-yielding base_rotation by A20, A29, A34, Th28, Th26;

                hence ex g be base_rotation Function of TR, TR st g is {k, z} -support-yielding & ((g . fp) . k) = (q . k) by A35;

              end;

            end;

            then

            consider g be base_rotation Function of TR, TR such that

             A36: g is {k, z} -support-yielding and

             A37: ((g . fp) . k) = (q . k);

            take gf = (g * f), Xmk;

            thus ( card Xmk) = m1 & Xmk c= ( Seg n) by A13, A14, A22, A24, CARD_2: 41, XBOOLE_1: 8;

            let m;

            

             A38: ( dom gf) = the carrier of TR by FUNCT_2: 52;

            

             A39: ( dom g) = the carrier of TR by FUNCT_2: 52;

            assume

             A40: m in Xmk;

            then

             A41: m in Xm or m in {k} by XBOOLE_0:def 3;

            per cases by A41, TARSKI:def 1;

              suppose

               A42: m in Xm;

              then m <> k by A17, XBOOLE_0:def 5;

              then not m in {k, z} by A26, A40, TARSKI:def 2;

              then ((g . fp) . m) = (fp . m) by A36, A39;

              

              hence ((gf . p) . m) = (fp . m) by A38, FUNCT_1: 12

              .= (q . m) by A15, A42;

            end;

              suppose m = k;

              hence ((gf . p) . m) = (q . m) by A37, A38, FUNCT_1: 12;

            end;

          end;

            suppose

             A43: for k st k in (( Seg n) \ Xm) holds (sfp . k) < (sq . k);

            

             A44: ( Sum sfp) >= 0 by RVSUM_1: 86;

            ( Sum sq) >= 0 & |.p.| = |.fp.| by Def4, RVSUM_1: 86;

            then

             A45: ( Sum sfp) = ( Sum sq) by A2, A44, SQUARE_1: 28;

            

             A46: ( len sfp) = ( len fp) by RVSUM_1: 143;

            

             A47: ( len sq) = ( len q) by RVSUM_1: 143;

            ( len fp) = n & ( len q) = n by CARD_1:def 7;

            then

            reconsider sfp, sq as Element of (n -tuples_on REAL ) by A46, A47, FINSEQ_2: 92;

            m < n by A16, NAT_1: 13;

            then Xm <> ( Seg n) by A13, FINSEQ_1: 57;

            then Xm c< ( Seg n) by A14, XBOOLE_0:def 8;

            then

            consider z be object such that

             A48: z in ( Seg n) and

             A49: not z in Xm by XBOOLE_0: 6;

            reconsider z as Nat by A48;

            

             A50: z in (( Seg n) \ Xm) by A48, A49, XBOOLE_0:def 5;

            for k st k in ( Seg n) holds (sfp . k) <= (sq . k)

            proof

              let k such that

               A51: k in ( Seg n);

              per cases by A51, XBOOLE_0:def 5;

                suppose k in (( Seg n) \ Xm);

                hence thesis by A43;

              end;

                suppose k in Xm;

                then (fp . k) = (q . k) by A15;

                

                then (sfp . k) = ((q . k) ^2 ) by VALUED_1: 11

                .= (sq . k) by VALUED_1: 11;

                hence thesis;

              end;

            end;

            then (sfp . z) >= (sq . z) by A45, A48, RVSUM_1: 83;

            hence thesis by A43, A50;

          end;

        end;

        reconsider n1 = (n - 1) as Nat by A5;

        

         A52: (n1 + 1) = n;

        

         A53: P[ 0 ]

        proof

          assume ( 0 + 1) <= n;

          take f = ( id TR), X = {} ;

          thus ( card X) = 0 & X c= ( Seg n);

          let k;

          assume k in X;

          hence thesis;

        end;

        for m holds P[m] from NAT_1:sch 2( A53, A10);

        then

        consider f be base_rotation Function of TR, TR, X be set such that

         A54: ( card X) = n1 & X c= ( Seg n) and

         A55: for k st k in X holds ((f . p) . k) = (q . k) by A52;

        ( card (( Seg n) \ X)) = (n - n1) by A9, A54, CARD_2: 44;

        then

        consider z be object such that

         A56: {z} = (( Seg n) \ X) by CARD_2: 42;

        set fp = (f . p);

        ( Sum ( sqr fp)) >= 0 & |.p.| = |.fp.| by Def4, RVSUM_1: 86;

        then

         A57: ( Sum ( sqr q)) = ( Sum ( sqr fp)) by A2, A8, SQUARE_1: 28;

        

         A58: z in {z} by TARSKI:def 1;

        then

         A59: z in ( Seg n) by A56, XBOOLE_0:def 5;

        reconsider z as Nat by A56, A58;

        set fpz = (fp +* (z,(q . z)));

        

         A60: ( len fp) = n by CARD_1:def 7;

        then

         A61: ( dom fp) = ( Seg n) by FINSEQ_1:def 3;

        

         A62: for k st 1 <= k & k <= n holds (fpz . k) = (q . k)

        proof

          let k;

          assume 1 <= k & k <= n;

          then

           A63: k in ( Seg n);

          per cases ;

            suppose k = z;

            hence thesis by A61, A63, FUNCT_7: 31;

          end;

            suppose

             A64: k <> z;

            then not k in (( Seg n) \ X) by A56, TARSKI:def 1;

            then

             A65: k in X by A63, XBOOLE_0:def 5;

            (fpz . k) = (fp . k) by A64, FUNCT_7: 32;

            hence thesis by A55, A65;

          end;

        end;

        

         A66: ( len fpz) = ( len fp) & ( len q) = n by CARD_1:def 7, FUNCT_7: 97;

        then

         A67: fpz = q by A60, A62;

        then

         A68: ( Sum ( sqr q)) = ((( Sum ( sqr fp)) - ((fp . z) ^2 )) + ((q . z) ^2 )) by A59, A61, Th3;

        per cases by A68, A57, SQUARE_1: 40;

          suppose (fp . z) = (q . z);

          then fp = q by A67, FUNCT_7: 35;

          hence thesis;

        end;

          suppose

           A69: (fp . z) = ( - (q . z));

          1 < n by A1, A7, XXREAL_0: 1;

          then (1 + 1) <= n by NAT_1: 13;

          then

          consider h be homogeneous additive Function of TR, TR such that

           A70: h is base_rotation and

           A71: (h . fp) = (fp +* (z,( - (fp . z)))) by A59, Th34;

          ( dom (h * f)) = the carrier of TR by FUNCT_2: 52;

          

          then ((h * f) . p) = (fp +* (z,( - (fp . z)))) by A71, FUNCT_1: 12

          .= q by A60, A62, A66, A69;

          hence thesis by A70;

        end;

      end;

    end;