vectmetr.miz



    begin

    definition

      let V be non empty MetrStruct;

      :: VECTMETR:def1

      attr V is convex means for x,y be Element of V holds for r be Real st 0 <= r & r <= 1 holds ex z be Element of V st ( dist (x,z)) = (r * ( dist (x,y))) & ( dist (z,y)) = ((1 - r) * ( dist (x,y)));

    end

    definition

      let V be non empty MetrStruct;

      :: VECTMETR:def2

      attr V is internal means for x,y be Element of V holds for p,q be Real st p > 0 & q > 0 holds ex f be FinSequence of the carrier of V st (f /. 1) = x & (f /. ( len f)) = y & (for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p) & for F be FinSequence of REAL st ( len F) = (( len f) - 1) & for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1)))) holds |.(( dist (x,y)) - ( Sum F)).| < q;

    end

    theorem :: VECTMETR:1

    

     Th1: for V be non empty MetrSpace st V is convex holds for x,y be Element of V holds for p be Real st p > 0 holds ex f be FinSequence of the carrier of V st (f /. 1) = x & (f /. ( len f)) = y & (for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p) & for F be FinSequence of REAL st ( len F) = (( len f) - 1) & for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1)))) holds ( dist (x,y)) = ( Sum F)

    proof

      let V be non empty MetrSpace;

      assume

       A1: V is convex;

      set A = the carrier of V;

      let x,y be Element of V;

      defpred P[ set, set, set] means for a1,a2 be Element of A st $1 = [a1, a2] holds ex b be Element of A st $2 = [a1, b] & $3 = [b, a2] & ( dist (a1,a2)) = (2 * ( dist (a1,b))) & ( dist (a1,a2)) = (2 * ( dist (b,a2)));

      

       A2: for a be Element of [:A, A:] holds ex c,d be Element of [:A, A:] st P[a, c, d]

      proof

        let a be Element of [:A, A:];

        consider a19,a29 be object such that

         A3: a19 in A & a29 in A and

         A4: a = [a19, a29] by ZFMISC_1:def 2;

        reconsider a19, a29 as Element of A by A3;

        consider z be Element of A such that

         A5: ( dist (a19,z)) = ((1 / 2) * ( dist (a19,a29))) and

         A6: ( dist (z,a29)) = ((1 - (1 / 2)) * ( dist (a19,a29))) by A1;

        take c = [a19, z];

        take d = [z, a29];

        let a1,a2 be Element of A;

        assume

         A7: a = [a1, a2];

        take z;

        thus c = [a1, z] by A4, A7, XTUPLE_0: 1;

        thus d = [z, a2] by A4, A7, XTUPLE_0: 1;

        a1 = a19 by A4, A7, XTUPLE_0: 1;

        hence ( dist (a1,a2)) = (2 * ( dist (a1,z))) by A4, A5, A7, XTUPLE_0: 1;

        a2 = a29 by A4, A7, XTUPLE_0: 1;

        hence thesis by A4, A6, A7, XTUPLE_0: 1;

      end;

      consider D be binary DecoratedTree of [:A, A:] such that

       A8: ( dom D) = ( { 0 , 1} * ) and

       A9: (D . {} ) = [x, y] and

       A10: for z be Node of D holds P[(D . z), (D . (z ^ <* 0 *>)), (D . (z ^ <*1*>))] from BINTREE2:sch 1( A2);

      reconsider dD = ( dom D) as full Tree by A8, BINTREE2:def 2;

      let p be Real such that

       A11: p > 0 ;

      per cases ;

        suppose ( dist (x,y)) >= p;

        then (( dist (x,y)) / p) >= 1 by A11, XREAL_1: 181;

        then ( log (2,(( dist (x,y)) / p))) >= ( log (2,1)) by PRE_FF: 10;

        then ( log (2,(( dist (x,y)) / p))) >= 0 by POWER: 51;

        then

        reconsider n1 = [\( log (2,(( dist (x,y)) / p)))/] as Element of NAT by INT_1: 53;

        defpred Q[ Nat] means for t be Tuple of $1, BOOLEAN st t = ( 0* $1) holds ((D . ( 'not' t)) `2 ) = y;

        defpred P[ Nat] means ((D . ( 0* $1)) `1 ) = x;

        reconsider n = (n1 + 1) as non zero Element of NAT ;

        reconsider N = (2 to_power n) as non zero Element of NAT by POWER: 34;

        set r = (( dist (x,y)) / N);

        reconsider FSL = ( FinSeqLevel (n,dD)) as FinSequence of ( dom D) by FINSEQ_2: 24;

        deffunc G( Nat) = (D . (FSL /. $1));

        consider g be FinSequence of [:A, A:] such that

         A12: ( len g) = N and

         A13: for k be Nat st k in ( dom g) holds (g . k) = G(k) from FINSEQ_2:sch 1;

        

         A14: ( dom g) = ( Seg N) by A12, FINSEQ_1:def 3;

        

         A15: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat;

          assume

           A16: ((D . ( 0* j)) `1 ) = x;

          reconsider zj = ( 0* j) as Node of D by A8, BINARI_3: 4;

          consider a,b be object such that

           A17: a in A & b in A and

           A18: (D . zj) = [a, b] by ZFMISC_1:def 2;

          reconsider a1 = a, b1 = b as Element of A by A17;

          

           A19: ex z1 be Element of A st (D . (zj ^ <* 0 *>)) = [a1, z1] & (D . (zj ^ <*1*>)) = [z1, b1] & ( dist (a1,b1)) = (2 * ( dist (a1,z1))) & ( dist (a1,b1)) = (2 * ( dist (z1,b1))) by A10, A18;

          

          thus ((D . ( 0* (j + 1))) `1 ) = ((D . (zj ^ <* 0 *>)) `1 ) by FINSEQ_2: 60

          .= a1 by A19

          .= x by A18, A16;

        end;

        

         A20: P[ 0 ] by A9;

        

         A21: for j be Nat holds P[j] from NAT_1:sch 2( A20, A15);

        (2 to_power n) > 0 by POWER: 34;

        then ( 0 + 1) <= (2 to_power n) by NAT_1: 13;

        then

         A22: 1 <= ( len ( FinSeqLevel (n,dD))) by BINTREE2: 19;

        

         A23: for j be non zero Nat st Q[j] holds Q[(j + 1)]

        proof

          let j be non zero Nat;

          assume

           A24: for t be Tuple of j, BOOLEAN st t = ( 0* j) holds ((D . ( 'not' t)) `2 ) = y;

          let t be Tuple of (j + 1), BOOLEAN ;

          consider t1 be Element of (j -tuples_on BOOLEAN ), dd be Element of BOOLEAN such that

           A25: t = (t1 ^ <*dd*>) by FINSEQ_2: 117;

          assume

           A26: t = ( 0* (j + 1));

          then t = (( 0* j) ^ <* 0 *>) by FINSEQ_2: 60;

          then t1 = ( 0* j) by A25, FINSEQ_2: 17;

          then

           A27: ((D . ( 'not' t1)) `2 ) = y by A24;

          dd = (t . (( len t1) + 1)) by A25, FINSEQ_1: 42

          .= (((j + 1) |-> 0 qua Real) . (j + 1)) by A26

          .= FALSE ;

          then ( 'not' dd) = 1;

          then

           A28: ( 'not' t) = (( 'not' t1) ^ <*1*>) by A25, BINARI_2: 9;

          reconsider nt1 = ( 'not' t1) as Node of D by A8, FINSEQ_1:def 11;

          consider a,b be object such that

           A29: a in A & b in A and

           A30: (D . nt1) = [a, b] by ZFMISC_1:def 2;

          reconsider a1 = a, b1 = b as Element of A by A29;

          ex b be Element of A st (D . (nt1 ^ <* 0 *>)) = [a1, b] & (D . (nt1 ^ <*1*>)) = [b, b1] & ( dist (a1,b1)) = (2 * ( dist (a1,b))) & ( dist (a1,b1)) = (2 * ( dist (b,b1))) by A10, A30;

          

          hence ((D . ( 'not' t)) `2 ) = b1 by A28

          .= y by A30, A27;

        end;

        

         A31: Q[1]

        proof

          reconsider pusty = ( <*> { 0 , 1}) as Node of D by A8, FINSEQ_1:def 11;

          let t be Tuple of 1, BOOLEAN ;

          

           A32: ex b be Element of A st (D . (pusty ^ <* 0 *>)) = [x, b] & (D . (pusty ^ <*1*>)) = [b, y] & ( dist (x,y)) = (2 * ( dist (x,b))) & ( dist (x,y)) = (2 * ( dist (b,y))) by A9, A10;

          assume t = ( 0* 1);

          then t = <* FALSE *> by FINSEQ_2: 59;

          

          hence ((D . ( 'not' t)) `2 ) = ((D . (pusty ^ <*1*>)) `2 ) by BINARI_3: 14, FINSEQ_1: 34

          .= y by A32;

        end;

        

         A33: for j be non zero Nat holds Q[j] from NAT_1:sch 10( A31, A23);

        deffunc F( Nat) = ((g /. $1) `1 );

        consider h be FinSequence of the carrier of V such that

         A34: ( len h) = N and

         A35: for k be Nat st k in ( dom h) holds (h . k) = F(k) from FINSEQ_2:sch 1;

        

         A36: ( dom h) = ( Seg N) by A34, FINSEQ_1:def 3;

        

         A37: 1 <= N by NAT_1: 14;

        then

         A38: 1 in ( Seg N) by FINSEQ_1: 1;

        then

         A39: 1 in ( dom h) by A34, FINSEQ_1:def 3;

        take f = (h ^ <*y*>);

        

         A40: ( len f) = (( len h) + ( len <*y*>)) by FINSEQ_1: 22

        .= (( len h) + 1) by FINSEQ_1: 39;

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

        

        hence (f /. 1) = (f . 1) by A34, A40, FINSEQ_4: 15

        .= (h . 1) by A39, FINSEQ_1:def 7

        .= ((g /. 1) `1 ) by A35, A36, A38

        .= ((g . 1) `1 ) by A12, A37, FINSEQ_4: 15

        .= ((D . (FSL /. 1)) `1 ) by A13, A14, A38

        .= ((D . (( FinSeqLevel (n,dD)) . 1)) `1 ) by A22, FINSEQ_4: 15

        .= ((D . ( 0* n)) `1 ) by BINTREE2: 15

        .= x by A21;

        ( len f) in ( Seg ( len f)) by A40, FINSEQ_1: 4;

        then ( len f) in ( dom f) by FINSEQ_1:def 3;

        

        hence

         A41: (f /. ( len f)) = ((h ^ <*y*>) . (( len h) + 1)) by A40, PARTFUN1:def 6

        .= y by FINSEQ_1: 42;

        

         A42: for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) = r

        proof

          ( 0* n) in ( BOOLEAN * ) by BINARI_3: 4;

          then

          reconsider ze = ( 0* n) as Tuple of n, BOOLEAN by FINSEQ_1:def 11;

          reconsider ze as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

          defpred S[ non zero Nat] means for j be non zero Element of NAT st j <= (2 to_power $1) holds for DF1,DF2 be Element of V st DF1 = ((D . (( FinSeqLevel ($1,dD)) . j)) `1 ) & DF2 = ((D . (( FinSeqLevel ($1,dD)) . j)) `2 ) holds ( dist (DF1,DF2)) = (( dist (x,y)) / (2 to_power $1));

          let i be Element of NAT ;

          assume that

           A43: 1 <= i and

           A44: i <= (( len f) - 1);

          

           A45: ( len FSL) = N by BINTREE2: 19;

           A46:

          now

            per cases by A44, XXREAL_0: 1;

              suppose i < (( len f) - 1);

              then i < (( len f) -' 1) by A40, NAT_1: 11, XREAL_1: 233;

              then (i + 1) <= (( len f) -' 1) by NAT_1: 13;

              then

               A47: (i + 1) <= (( len f) - 1) by A40, NAT_1: 11, XREAL_1: 233;

              then

               A48: ((i + 1) - 1) <= ((2 to_power n) - 1) by A34, A40, XREAL_1: 9;

              defpred R[ non zero Nat] means for i be Nat st 1 <= i & i <= ((2 to_power $1) - 1) holds ((D . (( FinSeqLevel ($1,dD)) . (i + 1))) `1 ) = ((D . (( FinSeqLevel ($1,dD)) . i)) `2 );

              

               A49: for n be non zero Nat st R[n] holds R[(n + 1)]

              proof

                let n be non zero Nat;

                reconsider nn = n as non zero Element of NAT by ORDINAL1:def 12;

                reconsider zb = (dD -level n) as non empty set by A8, BINTREE2: 10;

                assume

                 A50: for i be Nat st 1 <= i & i <= ((2 to_power n) - 1) holds ((D . (( FinSeqLevel (n,dD)) . (i + 1))) `1 ) = ((D . (( FinSeqLevel (n,dD)) . i)) `2 );

                let i be Nat;

                assume that

                 A51: 1 <= i and

                 A52: i <= ((2 to_power (n + 1)) - 1);

                reconsider ii = i as Element of NAT by ORDINAL1:def 12;

                

                 A53: (1 + 1) <= (i + 1) by A51, XREAL_1: 6;

                then

                 A54: ((i + 1) div 2) >= 1 by NAT_2: 13;

                (2 to_power (n + 1)) > 0 by POWER: 34;

                then

                 A55: (2 to_power (n + 1)) >= ( 0 + 1) by NAT_1: 13;

                then i <= ((2 to_power (n + 1)) -' 1) by A52, XREAL_1: 233;

                then i < (((2 to_power (n + 1)) -' 1) + 1) by NAT_1: 13;

                then

                 A56: i < (((2 to_power (n + 1)) - 1) + 1) by A55, XREAL_1: 233;

                then

                 A57: (i + 1) <= (2 to_power (n + 1)) by NAT_1: 13;

                then (i + 1) <= ((2 to_power n) * (2 to_power 1)) by POWER: 27;

                then (i + 1) <= ((2 to_power n) * 2) by POWER: 25;

                then

                 A58: (((i + 1) + 1) div 2) <= (2 to_power n) by NAT_2: 25;

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

                then 2 <= ((i + 1) + 1) by A53, XXREAL_0: 2;

                then (((i + 1) + 1) div 2) >= 1 by NAT_2: 13;

                then (((i + 1) + 1) div 2) in ( Seg (2 to_power n)) by A58, FINSEQ_1: 1;

                then (((i + 1) + 1) div 2) in ( dom ( FinSeqLevel (nn,dD))) by BINTREE2: 20;

                then (( FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2)) in zb by FINSEQ_2: 11;

                then

                reconsider FF = (( FinSeqLevel (nn,dD)) . (((i + 1) + 1) div 2)) as Tuple of n, BOOLEAN by BINTREE2: 5;

                reconsider FF as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

                reconsider FF1 = FF as Node of D by A8, FINSEQ_1:def 11;

                consider a9,b9 be object such that

                 A59: a9 in A & b9 in A and

                 A60: (D . FF1) = [a9, b9] by ZFMISC_1:def 2;

                i <= ((2 to_power n) * (2 to_power 1)) by A56, POWER: 27;

                then i <= ((2 to_power n) * 2) by POWER: 25;

                then ((i + 1) div 2) <= (2 to_power n) by NAT_2: 25;

                then ((i + 1) div 2) in ( Seg (2 to_power n)) by A54, FINSEQ_1: 1;

                then ((i + 1) div 2) in ( dom ( FinSeqLevel (nn,dD))) by BINTREE2: 20;

                then (( FinSeqLevel (n,dD)) . ((i + 1) div 2)) in zb by FINSEQ_2: 11;

                then

                reconsider F = (( FinSeqLevel (nn,dD)) . ((i + 1) div 2)) as Tuple of n, BOOLEAN by BINTREE2: 5;

                reconsider F as Element of (n -tuples_on BOOLEAN ) by FINSEQ_2: 131;

                reconsider F1 = F as Node of D by A8, FINSEQ_1:def 11;

                consider a,b be object such that

                 A61: a in A & b in A and

                 A62: (D . F1) = [a, b] by ZFMISC_1:def 2;

                reconsider a1 = a, b1 = b, a19 = a9, b19 = b9 as Element of A by A61, A59;

                consider d be Element of A such that

                 A63: (D . (F1 ^ <* 0 *>)) = [a1, d] and

                 A64: (D . (F1 ^ <*1*>)) = [d, b1] and ( dist (a1,b1)) = (2 * ( dist (a1,d))) and ( dist (a1,b1)) = (2 * ( dist (d,b1))) by A10, A62;

                consider d9 be Element of A such that

                 A65: (D . (FF1 ^ <* 0 *>)) = [a19, d9] and

                 A66: (D . (FF1 ^ <*1*>)) = [d9, b19] and ( dist (a19,b19)) = (2 * ( dist (a19,d9))) and ( dist (a19,b19)) = (2 * ( dist (d9,b19))) by A10, A60;

                

                 A67: i = ((i + 1) - 1)

                .= ((i + 1) -' 1) by NAT_1: 11, XREAL_1: 233;

                now

                  per cases ;

                    suppose i is odd;

                    then

                     A68: (i mod 2) = 1 by NAT_2: 22;

                    then ((i + 1) mod 2) = 0 by A67, NAT_2: 18;

                    then (i + 1) is even by NAT_2: 21;

                    then ((i + 1) div 2) = (((i + 1) + 1) div 2) by NAT_2: 26;

                    then

                     A69: d = d9 by A63, A65, XTUPLE_0: 1;

                    

                    thus ((D . (( FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 ) = ((D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 ) by A57, BINTREE2: 24

                    .= ((D . (FF ^ <*1*>)) `1 ) by A68, NAT_D: 21

                    .= d by A66, A69

                    .= ((D . (F ^ <* 0 *>)) `2 ) by A63

                    .= ((D . (F ^ <*((ii + 1) mod 2)*>)) `2 ) by A67, A68, NAT_2: 18

                    .= ((D . (( FinSeqLevel ((n + 1),dD)) . ii)) `2 ) by A51, A56, BINTREE2: 24;

                  end;

                    suppose i is even;

                    then

                     A70: (i mod 2) = 0 by NAT_2: 21;

                    

                    then

                     A71: 1 = ((i -' 1) mod 2) by A51, NAT_2: 18

                    .= (((i -' 1) + (2 * 1)) mod 2) by NAT_D: 21

                    .= ((((i -' 1) + 1) + 1) mod 2)

                    .= ((i + 1) mod 2) by A51, XREAL_1: 235;

                    

                     A72: (1 + (1 + i)) >= 1 by NAT_1: 11;

                    ((1 + 1) + (i -' 1)) = ((1 + 1) + (i - 1)) by A51, XREAL_1: 233

                    .= (((1 + 1) + i) - 1);

                    then 1 = ((((1 + 1) + i) -' 1) mod 2) by A71, A72, XREAL_1: 233;

                    then (((1 + 1) + i) mod 2) = 0 by NAT_2: 18;

                    then ((i + 1) + 1) = ((2 * (((i + 1) + 1) div 2)) + 0 ) by NAT_D: 2;

                    then

                     A73: 2 divides ((i + 1) + 1) by NAT_D: 3;

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

                    then ((((i + 1) + 1) -' 1) div 2) = ((((i + 1) + 1) div 2) - 1) by A73, NAT_2: 15;

                    then ((i + 1) div 2) = ((((i + 1) + 1) div 2) - 1) by NAT_D: 34;

                    then

                     A74: (((i + 1) div 2) + 1) = (((i + 1) + 1) div 2);

                    then

                     A75: ((i + 1) div 2) <= ((2 to_power n) - 1) by A58, XREAL_1: 19;

                    

                     A76: a9 = ((D . (( FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2))) `1 ) by A60

                    .= ((D . (( FinSeqLevel (n,dD)) . ((i + 1) div 2))) `2 ) by A50, A54, A74, A75

                    .= b by A62;

                    

                    thus ((D . (( FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 ) = ((D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 ) by A57, BINTREE2: 24

                    .= ((D . (FF ^ <* 0 *>)) `1 ) by A70, NAT_D: 21

                    .= a19 by A65

                    .= ((D . (F ^ <*1*>)) `2 ) by A64, A76

                    .= ((D . (( FinSeqLevel ((n + 1),dD)) . ii)) `2 ) by A51, A56, A71, BINTREE2: 24;

                  end;

                end;

                hence thesis;

              end;

              

               A77: R[1]

              proof

                reconsider pusty = ( <*> { 0 , 1}) as Node of D by A8, FINSEQ_1:def 11;

                let i be Nat;

                

                 A78: ((2 to_power 1) - 1) = ((1 + 1) - 1) by POWER: 25

                .= 1;

                consider b be Element of A such that

                 A79: (D . (pusty ^ <* 0 *>)) = [x, b] and

                 A80: (D . (pusty ^ <*1*>)) = [b, y] and ( dist (x,y)) = (2 * ( dist (x,b))) and ( dist (x,y)) = (2 * ( dist (b,y))) by A9, A10;

                assume 1 <= i & i <= ((2 to_power 1) - 1);

                then

                 A81: i = 1 by A78, XXREAL_0: 1;

                

                hence ((D . (( FinSeqLevel (1,dD)) . (i + 1))) `1 ) = ((D . <*1*>) `1 ) by BINTREE2: 23

                .= ((D . (pusty ^ <*1*>)) `1 ) by FINSEQ_1: 34

                .= b by A80

                .= ((D . (pusty ^ <* 0 *>)) `2 ) by A79

                .= ((D . <* 0 *>) `2 ) by FINSEQ_1: 34

                .= ((D . (( FinSeqLevel (1,dD)) . i)) `2 ) by A81, BINTREE2: 22;

              end;

              

               A82: for n be non zero Nat holds R[n] from NAT_1:sch 10( A77, A49);

              

               A83: 1 <= (1 + i) by NAT_1: 11;

              then

               A84: (i + 1) in ( Seg ( len h)) by A40, A47, FINSEQ_1: 1;

              then (i + 1) in ( dom h) by FINSEQ_1:def 3;

              

              hence (f /. (i + 1)) = (h /. (i + 1)) by FINSEQ_4: 68

              .= (h . (i + 1)) by A40, A47, A83, FINSEQ_4: 15

              .= ((g /. (i + 1)) `1 ) by A34, A35, A36, A84

              .= ((g . (i + 1)) `1 ) by A12, A34, A40, A47, A83, FINSEQ_4: 15

              .= ((D . (FSL /. (i + 1))) `1 ) by A13, A14, A34, A84

              .= ((D . (( FinSeqLevel (n,dD)) . (i + 1))) `1 ) by A34, A40, A45, A47, A83, FINSEQ_4: 15

              .= ((D . (( FinSeqLevel (n,dD)) . i)) `2 ) by A43, A48, A82;

            end;

              suppose

               A85: i = (( len f) - 1);

              

              hence (f /. (i + 1)) = ((D . ( 'not' ze)) `2 ) by A33, A41

              .= ((D . (( FinSeqLevel (n,dD)) . i)) `2 ) by A34, A40, A85, BINTREE2: 16;

            end;

          end;

          

           A86: for l be non zero Nat st S[l] holds S[(l + 1)]

          proof

            let l be non zero Nat;

            reconsider dDll = (dD -level l) as non empty set by A8, BINTREE2: 10;

            reconsider ll = l as non zero Element of NAT by ORDINAL1:def 12;

            reconsider dDll1 = (dD -level (l + 1)) as non empty set by A8, BINTREE2: 10;

            assume

             A87: for j be non zero Element of NAT st j <= (2 to_power l) holds for DF1,DF2 be Element of V st DF1 = ((D . (( FinSeqLevel (l,dD)) . j)) `1 ) & DF2 = ((D . (( FinSeqLevel (l,dD)) . j)) `2 ) holds ( dist (DF1,DF2)) = (( dist (x,y)) / (2 to_power l));

            let j be non zero Element of NAT ;

            ((j + 1) div 2) <> 0

            proof

              assume ((j + 1) div 2) = 0 ;

              then (j + 1) < (1 + 1) by NAT_2: 12;

              then j < 1 by XREAL_1: 6;

              hence contradiction by NAT_1: 14;

            end;

            then

            reconsider j1 = ((j + 1) div 2) as non zero Element of NAT ;

            assume

             A88: j <= (2 to_power (l + 1));

            then j <= ((2 to_power l) * (2 to_power 1)) by POWER: 27;

            then

             A89: j <= ((2 to_power l) * 2) by POWER: 25;

            then j1 >= 1 & j1 <= (2 to_power l) by NAT_1: 14, NAT_2: 25;

            then j1 in ( Seg (2 to_power l)) by FINSEQ_1: 1;

            then ((j + 1) div 2) in ( dom ( FinSeqLevel (ll,dD))) by BINTREE2: 20;

            then (( FinSeqLevel (l,dD)) . ((j + 1) div 2)) in dDll by FINSEQ_2: 11;

            then

            reconsider FSLlprim = (( FinSeqLevel (ll,dD)) . ((j + 1) div 2)) as Tuple of l, BOOLEAN by BINTREE2: 5;

            reconsider FSLlprim as Element of (l -tuples_on BOOLEAN ) by FINSEQ_2: 131;

            

             A90: ( FinSeqLevel ((l + 1),dD)) is FinSequence of ( dom D) by FINSEQ_2: 24;

            j >= 1 by NAT_1: 14;

            then j in ( Seg (2 to_power (l + 1))) by A88, FINSEQ_1: 1;

            then

             A91: j in ( dom ( FinSeqLevel ((l + 1),dD))) by BINTREE2: 20;

            then

            reconsider Fj = (( FinSeqLevel ((l + 1),dD)) . j) as Element of ( dom D) by A90, FINSEQ_2: 11;

            (( FinSeqLevel ((l + 1),dD)) . j) in dDll1 by A91, FINSEQ_2: 11;

            then

            reconsider FSLl1 = (( FinSeqLevel ((l + 1),dD)) . j) as Tuple of (l + 1), BOOLEAN by BINTREE2: 5;

            consider FSLl be Element of (l -tuples_on BOOLEAN ), d be Element of BOOLEAN such that

             A92: FSLl1 = (FSLl ^ <*d*>) by FINSEQ_2: 117;

            let DF1,DF2 be Element of V;

            assume DF1 = ((D . (( FinSeqLevel ((l + 1),dD)) . j)) `1 ) & DF2 = ((D . (( FinSeqLevel ((l + 1),dD)) . j)) `2 );

            then

             A93: (D . Fj) = [DF1, DF2] by MCART_1: 21;

            reconsider NFSLl = FSLl as Node of D by A8, FINSEQ_1:def 11;

            consider x1,y1 be object such that

             A94: x1 in A & y1 in A and

             A95: (D . NFSLl) = [x1, y1] by ZFMISC_1:def 2;

            reconsider x1, y1 as Element of A by A94;

            consider b be Element of A such that

             A96: (D . (NFSLl ^ <* 0 *>)) = [x1, b] and

             A97: (D . (NFSLl ^ <*1*>)) = [b, y1] and

             A98: ( dist (x1,y1)) = (2 * ( dist (x1,b))) and

             A99: ( dist (x1,y1)) = (2 * ( dist (b,y1))) by A10, A95;

            

             A100: (( FinSeqLevel ((ll + 1),dD)) . j) = (FSLlprim ^ <*((j + 1) mod 2)*>) by A88, BINTREE2: 24;

            then FSLl = FSLlprim by A92, FINSEQ_2: 17;

            then

             A101: x1 = ((D . (( FinSeqLevel (l,dD)) . j1)) `1 ) & y1 = ((D . (( FinSeqLevel (l,dD)) . j1)) `2 ) by A95;

            

             A102: d = ((j + 1) mod 2) by A92, A100, FINSEQ_2: 17;

            now

              per cases by A102, NAT_D: 12;

                suppose d = 0 ;

                then DF1 = x1 & DF2 = b by A93, A92, A96, XTUPLE_0: 1;

                then (2 * ( dist (DF1,DF2))) = (((( dist (x,y)) / (2 to_power l)) / 2) * 2) by A87, A89, A98, A101, NAT_2: 25;

                

                hence ( dist (DF1,DF2)) = (( dist (x,y)) / ((2 to_power l) * 2)) by XCMPLX_1: 78

                .= (( dist (x,y)) / ((2 to_power l) * (2 to_power 1))) by POWER: 25

                .= (( dist (x,y)) / (2 to_power (l + 1))) by POWER: 27;

              end;

                suppose d = 1;

                then DF1 = b & DF2 = y1 by A93, A92, A97, XTUPLE_0: 1;

                then (2 * ( dist (DF1,DF2))) = (((( dist (x,y)) / (2 to_power l)) / 2) * 2) by A87, A89, A99, A101, NAT_2: 25;

                

                hence ( dist (DF1,DF2)) = (( dist (x,y)) / ((2 to_power l) * 2)) by XCMPLX_1: 78

                .= (( dist (x,y)) / ((2 to_power l) * (2 to_power 1))) by POWER: 25

                .= (( dist (x,y)) / (2 to_power (l + 1))) by POWER: 27;

              end;

            end;

            hence thesis;

          end;

          

           A103: S[1]

          proof

            reconsider pusty = ( <*> { 0 , 1}) as Node of D by A8, FINSEQ_1:def 11;

            let j be non zero Element of NAT ;

            assume

             A104: j <= (2 to_power 1);

            

             A105: ( FinSeqLevel (1,dD)) is FinSequence of ( dom D) by FINSEQ_2: 24;

            j >= 1 by NAT_1: 14;

            then j in ( Seg (2 to_power 1)) by A104, FINSEQ_1: 1;

            then j in ( dom ( FinSeqLevel (1,dD))) by BINTREE2: 20;

            then

            reconsider FSL1j = (( FinSeqLevel (1,dD)) . j) as Element of ( dom D) by A105, FINSEQ_2: 11;

            let DF1,DF2 be Element of V;

            assume

             A106: DF1 = ((D . (( FinSeqLevel (1,dD)) . j)) `1 ) & DF2 = ((D . (( FinSeqLevel (1,dD)) . j)) `2 );

            (2 to_power 1) = 2 & j >= 1 by NAT_1: 14, POWER: 25;

            then

             A107: j in ( Seg 2) by A104, FINSEQ_1: 1;

            now

              per cases by A107, FINSEQ_1: 2, TARSKI:def 2;

                suppose

                 A108: j = 1;

                

                 A109: ex b be Element of A st (D . (pusty ^ <* 0 *>)) = [x, b] & (D . (pusty ^ <*1*>)) = [b, y] & ( dist (x,y)) = (2 * ( dist (x,b))) & ( dist (x,y)) = (2 * ( dist (b,y))) by A9, A10;

                

                 A110: (D . (pusty ^ <* 0 *>)) = (D . <* 0 *>) by FINSEQ_1: 34

                .= (D . FSL1j) by A108, BINTREE2: 22

                .= [DF1, DF2] by A106, MCART_1: 21;

                then DF1 = x by A109, XTUPLE_0: 1;

                hence ( dist (DF1,DF2)) = (( dist (x,y)) / 2) by A110, A109, XTUPLE_0: 1;

              end;

                suppose

                 A111: j = 2;

                consider b be Element of A such that (D . (pusty ^ <* 0 *>)) = [x, b] and

                 A112: (D . (pusty ^ <*1*>)) = [b, y] and ( dist (x,y)) = (2 * ( dist (x,b))) and

                 A113: ( dist (x,y)) = (2 * ( dist (b,y))) by A9, A10;

                

                 A114: (D . (pusty ^ <*1*>)) = (D . <*1*>) by FINSEQ_1: 34

                .= (D . FSL1j) by A111, BINTREE2: 23

                .= [DF1, DF2] by A106, MCART_1: 21;

                then DF1 = b by A112, XTUPLE_0: 1;

                hence ( dist (DF1,DF2)) = (( dist (x,y)) / 2) by A114, A112, A113, XTUPLE_0: 1;

              end;

            end;

            hence thesis by POWER: 25;

          end;

          

           A115: for l be non zero Nat holds S[l] from NAT_1:sch 10( A103, A86);

          

           A116: i in ( Seg ( len h)) by A40, A43, A44, FINSEQ_1: 1;

          then i in ( dom h) by FINSEQ_1:def 3;

          

          then (f /. i) = (h /. i) by FINSEQ_4: 68

          .= (h . i) by A40, A43, A44, FINSEQ_4: 15

          .= ((g /. i) `1 ) by A34, A35, A36, A116

          .= ((g . i) `1 ) by A12, A34, A40, A43, A44, FINSEQ_4: 15

          .= ((D . (FSL /. i)) `1 ) by A13, A14, A34, A116

          .= ((D . (( FinSeqLevel (n,dD)) . i)) `1 ) by A34, A40, A43, A44, A45, FINSEQ_4: 15;

          hence thesis by A34, A40, A43, A44, A46, A115;

        end;

        ( log (2,(( dist (x,y)) / p))) < (n * 1) by INT_1: 29;

        then ( log (2,(( dist (x,y)) / p))) < (n * ( log (2,2))) by POWER: 52;

        then ( log (2,(( dist (x,y)) / p))) < ( log (2,(2 to_power n))) by POWER: 55;

        then (( dist (x,y)) / p) < N by PRE_FF: 10;

        then ((( dist (x,y)) / p) * p) < (N * p) by A11, XREAL_1: 68;

        then ( dist (x,y)) < (N * p) by A11, XCMPLX_1: 87;

        then (( dist (x,y)) / N) < ((N * p) / N) by XREAL_1: 74;

        then (( dist (x,y)) / N) < ((p / N) * N) by XCMPLX_1: 74;

        then r < p by XCMPLX_1: 87;

        hence for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p by A42;

        let F be FinSequence of REAL such that

         A117: ( len F) = (( len f) - 1) and

         A118: for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1))));

        

         A119: ( rng F) = {r}

        proof

          thus ( rng F) c= {r}

          proof

            let a be object;

            assume a in ( rng F);

            then

            consider c be object such that

             A120: c in ( dom F) and

             A121: (F . c) = a by FUNCT_1:def 3;

            c in ( Seg ( len F)) by A120, FINSEQ_1:def 3;

            then c in { t where t be Nat : 1 <= t & t <= ( len F) } by FINSEQ_1:def 1;

            then

            consider c1 be Nat such that

             A122: c1 = c and

             A123: 1 <= c1 & c1 <= ( len F);

            reconsider c1 as Element of NAT by ORDINAL1:def 12;

            a = (F /. c1) by A121, A122, A123, FINSEQ_4: 15

            .= ( dist ((f /. c1),(f /. (c1 + 1)))) by A118, A123

            .= r by A42, A117, A123;

            hence thesis by TARSKI:def 1;

          end;

          let a be object;

          assume a in {r};

          then a = r by TARSKI:def 1;

          

          then

           A124: a = ( dist ((f /. 1),(f /. (1 + 1)))) by A34, A40, A37, A42

          .= (F /. 1) by A34, A40, A37, A117, A118

          .= (F . 1) by A34, A40, A37, A117, FINSEQ_4: 15;

          1 in ( Seg ( len F)) by A34, A40, A37, A117, FINSEQ_1: 1;

          then 1 in ( dom F) by FINSEQ_1:def 3;

          hence thesis by A124, FUNCT_1:def 3;

        end;

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

        then F = (( len F) |-> r) by A119, FUNCOP_1: 9;

        

        hence ( Sum F) = (((N + 1) - 1) * r) by A34, A40, A117, RVSUM_1: 80

        .= ( dist (x,y)) by XCMPLX_1: 87;

      end;

        suppose

         A125: ( dist (x,y)) < p;

        take f = <*x, y*>;

        thus

         A126: (f /. 1) = x by FINSEQ_4: 17;

        ( len f) = 2 by FINSEQ_1: 44;

        hence (f /. ( len f)) = y by FINSEQ_4: 17;

        

         A127: (( len f) - 1) = ((1 + 1) - 1) by FINSEQ_1: 44

        .= 1;

        thus for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p

        proof

          let i be Element of NAT ;

          assume 1 <= i & i <= (( len f) - 1);

          then i in ( Seg 1) by A127, FINSEQ_1: 1;

          then i = 1 by FINSEQ_1: 2, TARSKI:def 1;

          hence thesis by A125, A126, FINSEQ_4: 17;

        end;

        let F be FinSequence of REAL ;

        assume that

         A128: ( len F) = (( len f) - 1) and

         A129: for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1))));

        reconsider dxy = ( dist (x,y)) as Element of REAL by XREAL_0:def 1;

        1 <= ( len F) by A127, A128;

        then 1 in ( dom F) by FINSEQ_3: 25;

        then (F /. 1) = (F . 1) by PARTFUN1:def 6;

        

        then (F . 1) = ( dist ((f /. 1),(f /. (1 + 1)))) by A127, A128, A129

        .= ( dist (x,y)) by A126, FINSEQ_4: 17;

        then F = <*dxy*> by A127, A128, FINSEQ_5: 14;

        then ( Sum F) = dxy by FINSOP_1: 11;

        hence thesis;

      end;

    end;

    registration

      cluster convex -> internal for non empty MetrSpace;

      coherence

      proof

        let V be non empty MetrSpace;

        assume

         A1: V is convex;

        let x,y be Element of V;

        let p,q be Real such that

         A2: p > 0 and

         A3: q > 0 ;

        consider f be FinSequence of the carrier of V such that

         A4: (f /. 1) = x & (f /. ( len f)) = y & for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p and

         A5: for F be FinSequence of REAL st ( len F) = (( len f) - 1) & for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1)))) holds ( dist (x,y)) = ( Sum F) by A1, A2, Th1;

        take f;

        thus (f /. 1) = x & (f /. ( len f)) = y & for i be Element of NAT st 1 <= i & i <= (( len f) - 1) holds ( dist ((f /. i),(f /. (i + 1)))) < p by A4;

        let F be FinSequence of REAL ;

        assume ( len F) = (( len f) - 1) & for i be Element of NAT st 1 <= i & i <= ( len F) holds (F /. i) = ( dist ((f /. i),(f /. (i + 1))));

        then ( dist (x,y)) = ( Sum F) by A5;

        hence |.(( dist (x,y)) - ( Sum F)).| < q by A3, ABSVALUE: 2;

      end;

    end

    registration

      cluster convex for non empty MetrSpace;

      existence

      proof

        reconsider ZS = { 0 } as non empty set;

        deffunc T( Element of ZS, Element of ZS) = ( In ( 0 , REAL ));

        consider F be Function of [:ZS, ZS:], REAL such that

         A1: for x,y be Element of ZS holds (F . (x,y)) = T(x,y) from BINOP_1:sch 4;

        reconsider V = MetrStruct (# ZS, F #) as non empty MetrStruct;

         A2:

        now

          let a,b be Element of V;

          

          thus ( dist (a,b)) = (F . (a,b)) by METRIC_1:def 1

          .= 0 by A1

          .= (F . (b,a)) by A1

          .= ( dist (b,a)) by METRIC_1:def 1;

        end;

         A3:

        now

          let a be Element of V;

          

          thus ( dist (a,a)) = (F . (a,a)) by METRIC_1:def 1

          .= 0 by A1;

        end;

         A4:

        now

          let a,b,c be Element of V;

          

           A5: c = 0 by TARSKI:def 1;

          a = 0 by TARSKI:def 1;

          then b = 0 & ( dist (a,c)) = 0 by A3, A5, TARSKI:def 1;

          hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A3, A5;

        end;

        now

          let a,b be Element of V;

          assume ( dist (a,b)) = 0 ;

          a = 0 by TARSKI:def 1;

          hence a = b by TARSKI:def 1;

        end;

        then

        reconsider V as discerning Reflexive symmetric triangle non empty MetrStruct by A3, A2, A4, METRIC_1: 1, METRIC_1: 2, METRIC_1: 3, METRIC_1: 4;

        take V;

        let x,y be Element of V;

        let r be Real such that 0 <= r and r <= 1;

        take z = x;

        

         A6: ( dist (z,y)) = (F . (z,y)) by METRIC_1:def 1

        .= 0 by A1;

        ( dist (x,z)) = (F . (x,z)) by METRIC_1:def 1

        .= 0 by A1;

        hence ( dist (x,z)) = (r * ( dist (x,y))) & ( dist (z,y)) = ((1 - r) * ( dist (x,y))) by A6;

      end;

    end

    begin

    definition

      let V be non empty MetrStruct;

      let f be Function of V, V;

      :: VECTMETR:def3

      attr f is isometric means

      : Def3: for x,y be Element of V holds ( dist (x,y)) = ( dist ((f . x),(f . y)));

    end

    registration

      let V be non empty MetrStruct;

      cluster ( id V) -> onto isometric;

      coherence

      proof

        thus ( rng ( id V)) = the carrier of V;

        let x,y be Element of V;

        

        thus ( dist (x,y)) = ( dist ((( id V) . x),y))

        .= ( dist ((( id V) . x),(( id V) . y)));

      end;

    end

    theorem :: VECTMETR:2

    for V be non empty MetrStruct holds ( id V) is onto isometric;

    registration

      let V be non empty MetrStruct;

      cluster onto isometric for Function of V, V;

      existence

      proof

        take f = ( id the carrier of V);

        thus ( rng f) = the carrier of V;

        let x,y be Element of V;

        

        thus ( dist (x,y)) = ( dist ((f . x),y))

        .= ( dist ((f . x),(f . y)));

      end;

    end

    definition

      let V be non empty MetrStruct;

      defpred P[ object] means $1 is onto isometric Function of V, V;

      :: VECTMETR:def4

      func ISOM (V) -> set means

      : Def4: for x be object holds x in it iff x is onto isometric Function of V, V;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (the carrier of V,the carrier of V)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        thus x in X implies x is onto isometric Function of V, V by A1;

        assume

         A2: x is onto isometric Function of V, V;

        then x in ( Funcs (the carrier of V,the carrier of V)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    definition

      let V be non empty MetrStruct;

      :: original: ISOM

      redefine

      func ISOM (V) -> Subset of ( Funcs (the carrier of V,the carrier of V)) ;

      coherence

      proof

        now

          let x be object;

          assume x in ( ISOM V);

          then x is Function of V, V by Def4;

          hence x in ( Funcs (the carrier of V,the carrier of V)) by FUNCT_2: 8;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let V be discerning Reflexive non empty MetrStruct;

      cluster isometric -> one-to-one for Function of V, V;

      coherence

      proof

        let f be Function of V, V;

        assume

         A1: f is isometric;

        now

          let x,y be object;

          assume that

           A2: x in ( dom f) & y in ( dom f) and

           A3: (f . x) = (f . y);

          reconsider x1 = x, y1 = y as Element of V by A2;

          ( dist (x1,y1)) = ( dist ((f . x1),(f . y1))) by A1

          .= 0 by A3, METRIC_1: 1;

          hence x = y by METRIC_1: 2;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

    end

    registration

      let V be discerning Reflexive non empty MetrStruct;

      let f be onto isometric Function of V, V;

      cluster (f " ) -> onto isometric;

      coherence

      proof

        

         A1: ( rng f) = ( [#] V) by FUNCT_2:def 3;

        hence ( rng (f " )) = the carrier of V by TOPS_2: 49;

        let x,y be Element of V;

        

         A2: ( rng f) = the carrier of V by A1;

        then

         A3: ( dom (f " )) = ( [#] V) by TOPS_2: 49;

        

         A4: y = (( id ( rng f)) . y) by A2

        .= ((f * (f " )) . y) by A1, TOPS_2: 52

        .= (f . ((f " ) . y)) by A3, FUNCT_1: 13;

        x = (( id ( rng f)) . x) by A2

        .= ((f * (f " )) . x) by A1, TOPS_2: 52

        .= (f . ((f " ) . x)) by A3, FUNCT_1: 13;

        hence thesis by A4, Def3;

      end;

    end

    registration

      let V be non empty MetrStruct;

      let f,g be onto isometric Function of V, V;

      cluster (f * g) -> onto isometric;

      coherence

      proof

        (f * g) is onto isometric

        proof

          ( rng g) = the carrier of V by FUNCT_2:def 3

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

          

          hence ( rng (f * g)) = ( rng f) by RELAT_1: 28

          .= the carrier of V by FUNCT_2:def 3;

          let x,y be Element of V;

          x in the carrier of V;

          then

           A1: x in ( dom g) by FUNCT_2:def 1;

          y in the carrier of V;

          then

           A2: y in ( dom g) by FUNCT_2:def 1;

          

          thus ( dist (x,y)) = ( dist ((g . x),(g . y))) by Def3

          .= ( dist ((f . (g . x)),(f . (g . y)))) by Def3

          .= ( dist (((f * g) . x),(f . (g . y)))) by A1, FUNCT_1: 13

          .= ( dist (((f * g) . x),((f * g) . y))) by A2, FUNCT_1: 13;

        end;

        hence thesis;

      end;

    end

    registration

      let V be non empty MetrStruct;

      cluster ( ISOM V) -> non empty;

      coherence

      proof

        ( id V) is onto isometric;

        hence thesis by Def4;

      end;

    end

    begin

    definition

      struct ( RLSStruct, MetrStruct) RLSMetrStruct (# the carrier -> set,

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

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

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

       attr strict strict;

    end

    registration

      cluster non empty strict for RLSMetrStruct;

      existence

      proof

        set X = the non empty set, F = the Function of [:X, X:], REAL , O = the Element of X, B = the BinOp of X, G = the Function of [: REAL , X:], X;

        take RLSMetrStruct (# X, F, O, B, G #);

        thus the carrier of RLSMetrStruct (# X, F, O, B, G #) is non empty;

        thus thesis;

      end;

    end

    registration

      let X be non empty set;

      let F be Function of [:X, X:], REAL ;

      let O be Element of X;

      let B be BinOp of X;

      let G be Function of [: REAL , X:], X;

      cluster RLSMetrStruct (# X, F, O, B, G #) -> non empty;

      coherence ;

    end

    definition

      let V be non empty RLSMetrStruct;

      :: VECTMETR:def5

      attr V is homogeneous means

      : Def5: for r be Real holds for v,w be Element of V holds ( dist ((r * v),(r * w))) = ( |.r.| * ( dist (v,w)));

    end

    definition

      let V be non empty RLSMetrStruct;

      :: VECTMETR:def6

      attr V is translatible means

      : Def6: for u,w,v be Element of V holds ( dist (v,w)) = ( dist ((v + u),(w + u)));

    end

    definition

      let V be non empty RLSMetrStruct;

      let v be Element of V;

      :: VECTMETR:def7

      func Norm (v) -> Real equals ( dist (( 0. V),v));

      coherence ;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Reflexive discerning symmetric triangle homogeneous translatible for non empty RLSMetrStruct;

      existence

      proof

        reconsider ZS = { 0 } as non empty set;

        reconsider O = 0 as Element of ZS by TARSKI:def 1;

        deffunc T( Element of ZS, Element of ZS) = ( In ( 0 , REAL ));

        consider FF be Function of [:ZS, ZS:], REAL such that

         A1: for x,y be Element of ZS holds (FF . (x,y)) = T(x,y) from BINOP_1:sch 4;

        deffunc M( Real, Element of ZS) = O;

        deffunc A( Element of ZS, Element of ZS) = O;

        consider F be BinOp of ZS such that

         A2: for x,y be Element of ZS holds (F . (x,y)) = A(x,y) from BINOP_1:sch 4;

        consider G be Function of [: REAL , ZS:], ZS such that

         A3: for a be Element of REAL holds for x be Element of ZS holds (G . (a,x)) = M(a,x) from BINOP_1:sch 4;

        

         A4: for a be Real holds for x be Element of ZS holds (G . (a,x)) = M(a,x)

        proof

          let a be Real, x be Element of ZS;

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

          (G . (a,x)) = M(a,x) by A3;

          hence thesis;

        end;

        set W = RLSMetrStruct (# ZS, FF, O, F, G #);

        

         A5: for a,b be Real holds for x be VECTOR of W holds ((a + b) * x) = ((a * x) + (b * x))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let x be VECTOR of W;

          set c = (a + b);

          reconsider X = x as Element of ZS;

          (c * x) = M(c,X) by A4;

          hence thesis by A2;

        end;

        take W;

        thus W is strict;

        for x,y be VECTOR of W holds (x + y) = (y + x)

        proof

          let x,y be VECTOR of W;

          reconsider X = x, Y = y as Element of ZS;

          (x + y) = A(X,Y) by A2;

          hence thesis by A2;

        end;

        hence W is Abelian;

        for x,y,z be VECTOR of W holds ((x + y) + z) = (x + (y + z))

        proof

          let x,y,z be VECTOR of W;

          reconsider X = x, Y = y, Z = z as Element of ZS;

          ((x + y) + z) = A(A,Z) by A2;

          hence thesis by A2;

        end;

        hence W is add-associative;

        for x be VECTOR of W holds (x + ( 0. W)) = x

        proof

          let x be VECTOR of W;

          reconsider X = x as Element of ZS;

          (x + ( 0. W)) = A(X,O) by A2;

          hence thesis by TARSKI:def 1;

        end;

        hence W is right_zeroed;

        thus W is right_complementable

        proof

          reconsider y = O as VECTOR of W;

          let x be VECTOR of W;

          take y;

          thus thesis by A2;

        end;

        

         A6: for a be Real holds for x,y be VECTOR of W holds (a * (x + y)) = ((a * x) + (a * y))

        proof

          let a be Real;

          reconsider a as Real;

          let x,y be VECTOR of W;

          reconsider X = x, Y = y as Element of ZS;

          ((a * x) + (a * y)) = A(M,M) by A2;

          hence thesis by A4;

        end;

        

         A7: for a,b be Real holds for x be VECTOR of W holds ((a * b) * x) = (a * (b * x))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let x be VECTOR of W;

          set c = (a * b);

          reconsider X = x as Element of ZS;

          (c * x) = M(c,X) by A4;

          hence thesis by A4;

        end;

        for x be VECTOR of W holds (1 * x) = x

        proof

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

          let x be VECTOR of W;

          reconsider X = x as Element of ZS;

          (1 * x) = M(A9,X) by A4;

          hence thesis by TARSKI:def 1;

        end;

        hence W is vector-distributive scalar-distributive scalar-associative scalar-unital by A6, A5, A7;

        

         A8: for a,b,c be Point of W holds ( dist (a,a)) = 0 & (( dist (a,b)) = 0 implies a = b) & ( dist (a,b)) = ( dist (b,a)) & ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)))

        proof

          let a,b,c be Point of W;

          

           A9: ( dist (a,a)) = (FF . (a,a)) by METRIC_1:def 1

          .= 0 by A1;

          hence ( dist (a,a)) = 0 ;

          

           A10: a = 0 by TARSKI:def 1;

          hence ( dist (a,b)) = 0 implies a = b by TARSKI:def 1;

          

           A11: b = 0 by TARSKI:def 1;

          hence ( dist (a,b)) = ( dist (b,a)) by A10;

          thus thesis by A10, A11, A9;

        end;

        hence W is Reflexive by METRIC_1: 1;

        thus W is discerning by A8, METRIC_1: 2;

        thus W is symmetric by A8, METRIC_1: 3;

        thus W is triangle by A8, METRIC_1: 4;

        for r be Real holds for v,w be VECTOR of W holds ( dist ((r * v),(r * w))) = ( |.r.| * ( dist (v,w)))

        proof

          let r be Real;

          let v,w be VECTOR of W;

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

          

           A12: (FF . (v1,w1)) = T(v1,w1) by A1;

          

          thus ( dist ((r * v),(r * w))) = (FF . ((r * v),(r * w))) by METRIC_1:def 1

          .= ( |.r.| * 0 ) by A1

          .= ( |.r.| * T(v1,w1))

          .= ( |.r.| * (FF . (v1,w1))) by A12

          .= ( |.r.| * ( dist (v,w))) by METRIC_1:def 1;

        end;

        hence W is homogeneous;

        for u,w,v be VECTOR of W holds ( dist (v,w)) = ( dist ((v + u),(w + u)))

        proof

          let u,w,v be VECTOR of W;

          

          thus ( dist ((v + u),(w + u))) = (FF . ((v + u),(w + u))) by METRIC_1:def 1

          .= 0 by A1

          .= (FF . (v,w)) by A1

          .= ( dist (v,w)) by METRIC_1:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      mode RealLinearMetrSpace is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Reflexive discerning symmetric triangle homogeneous translatible non empty RLSMetrStruct;

    end

    ::$Canceled

    theorem :: VECTMETR:6

    for V be homogeneous Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSMetrStruct holds for r be Real holds for v be Element of V holds ( Norm (r * v)) = ( |.r.| * ( Norm v))

    proof

      let V be homogeneous Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSMetrStruct;

      let r be Real;

      let v be Element of V;

      

      thus ( Norm (r * v)) = ( dist ((r * ( 0. V)),(r * v))) by RLVECT_1: 10

      .= ( |.r.| * ( Norm v)) by Def5;

    end;

    theorem :: VECTMETR:7

    for V be translatible Abelian add-associative right_zeroed right_complementable triangle non empty RLSMetrStruct holds for v,w be Element of V holds ( Norm (v + w)) <= (( Norm v) + ( Norm w))

    proof

      let V be translatible Abelian add-associative right_zeroed right_complementable triangle non empty RLSMetrStruct;

      let v,w be Element of V;

      ( Norm (v + w)) <= (( dist (( 0. V),v)) + ( dist (v,(v + w)))) by METRIC_1: 4;

      then ( Norm (v + w)) <= (( Norm v) + ( dist ((v + ( - v)),((v + w) + ( - v))))) by Def6;

      then ( Norm (v + w)) <= (( Norm v) + ( dist (( 0. V),((v + w) + ( - v))))) by RLVECT_1: 5;

      then ( Norm (v + w)) <= (( Norm v) + ( dist (( 0. V),(w + (( - v) + v))))) by RLVECT_1:def 3;

      then ( Norm (v + w)) <= (( Norm v) + ( dist (( 0. V),(w + ( 0. V))))) by RLVECT_1: 5;

      hence thesis by RLVECT_1: 4;

    end;

    theorem :: VECTMETR:8

    for V be translatible add-associative right_zeroed right_complementable non empty RLSMetrStruct holds for v,w be Element of V holds ( dist (v,w)) = ( Norm (w - v))

    proof

      let V be translatible add-associative right_zeroed right_complementable non empty RLSMetrStruct;

      let v,w be Element of V;

      

      thus ( dist (v,w)) = ( dist ((v + ( - v)),(w + ( - v)))) by Def6

      .= ( Norm (w - v)) by RLVECT_1: 5;

    end;

    definition

      let n be Element of NAT ;

      :: VECTMETR:def8

      func RLMSpace n -> strict RealLinearMetrSpace means

      : Def8: the carrier of it = ( REAL n) & the distance of it = ( Pitag_dist n) & ( 0. it ) = ( 0* n) & (for x,y be Element of ( REAL n) holds (the addF of it . (x,y)) = (x + y)) & for x be Element of ( REAL n), r be Element of REAL holds (the Mult of it . (r,x)) = (r * x);

      existence

      proof

        deffunc G( Real, Element of ( REAL n)) = ($1 * $2);

        deffunc F( Element of ( REAL n), Element of ( REAL n)) = ($1 + $2);

        consider f be BinOp of ( REAL n) such that

         A1: for x,y be Element of ( REAL n) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        consider g be Function of [: REAL , ( REAL n):], ( REAL n) such that

         A2: for r be Element of REAL , x be Element of ( REAL n) holds (g . (r,x)) = G(r,x) from BINOP_1:sch 4;

        set RLSMS = RLSMetrStruct (# ( REAL n), ( Pitag_dist n), ( 0* n), f, g #);

        

         A3: for r be Real, x be Element of ( REAL n) holds (g . (r,x)) = G(r,x)

        proof

          let r be Real, x be Element of ( REAL n);

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

          (g . (r,x)) = G(r,x) by A2;

          hence thesis;

        end;

         A4:

        now

          let u,v,w be Element of RLSMS;

          reconsider u1 = u, v1 = v, w1 = w as Element of ( REAL n);

          

          thus ((u + v) + w) = (f . ((u1 + v1),w)) by A1

          .= ((u1 + v1) + w1) by A1

          .= (u1 + (v1 + w1)) by FINSEQOP: 28

          .= (f . (u,(v1 + w1))) by A1

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

        end;

         A5:

        now

          let v,w be Element of RLSMS;

          reconsider v1 = v, w1 = w as Element of ( REAL n);

          

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

          .= (w + v) by A1;

        end;

         A6:

        now

          let v be Element of RLSMS;

          reconsider v1 = v as Element of (n -tuples_on REAL );

          

          thus (v + ( 0. RLSMS)) = (v1 + (n |-> ( In ( 0 , REAL )))) by A1

          .= v by RVSUM_1: 16;

        end;

         A7:

        now

          let r be Real, v,w be VECTOR of RLSMS;

          reconsider v1 = v, w1 = w as Element of ( REAL n);

          reconsider v2 = v1, w2 = w1 as Element of (n -tuples_on REAL );

          

           A8: ( dist (v,w)) = (( Pitag_dist n) . (v,w)) by METRIC_1:def 1

          .= |.(v1 - w1).| by EUCLID:def 6;

          

           A9: (r * v) = (r * v1) & (r * w) = (r * w1) by A3;

          

          thus ( dist ((r * v),(r * w))) = (( Pitag_dist n) . ((r * v),(r * w))) by METRIC_1:def 1

          .= |.((r * v2) - (r * w2)).| by A9, EUCLID:def 6

          .= |.((r * v2) + ((( - 1) * r) * w2)).| by RVSUM_1: 49

          .= |.((r * v2) + (r * ( - w2))).| by RVSUM_1: 49

          .= |.(r * (v1 - w1)).| by RVSUM_1: 51

          .= ( |.r.| * ( dist (v,w))) by A8, EUCLID: 11;

        end;

         A10:

        now

          let u,w,v be VECTOR of RLSMS;

          reconsider u1 = u, w1 = w, v1 = v as Element of ( REAL n);

          reconsider u2 = u1, w2 = w1, v2 = v1 as Element of (n -tuples_on REAL );

          

           A11: (v + u) = (v1 + u1) & (w + u) = (w1 + u1) by A1;

          

          thus ( dist (v,w)) = (( Pitag_dist n) . (v,w)) by METRIC_1:def 1

          .= |.(v1 - w1).| by EUCLID:def 6

          .= |.(((v2 + u2) - u2) - w2).| by RVSUM_1: 42

          .= |.((v2 + u2) - (u2 + w2)).| by RVSUM_1: 39

          .= (( Pitag_dist n) . ((v1 + u1),(w1 + u1))) by EUCLID:def 6

          .= ( dist ((v + u),(w + u))) by A11, METRIC_1:def 1;

        end;

        

         A12: RLSMS is right_complementable

        proof

          let v be Element of RLSMS;

          reconsider v1 = v as Element of (n -tuples_on REAL );

          reconsider w = ( - v1) as Element of RLSMS;

          take w;

          

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

          .= ( 0. RLSMS) by RVSUM_1: 37;

        end;

         A13:

        now

          hereby

            let a1 be Real, v,w be VECTOR of RLSMS;

            reconsider a = a1 as Real;

            reconsider v1 = v, w1 = w as Element of ( REAL n);

            reconsider v2 = v1, w2 = w1 as Element of (n -tuples_on REAL );

            (a * (v + w)) = (g . (a,(v1 + w1))) by A1

            .= (a * (v2 + w2)) by A3

            .= ((a * v1) + (a * w1)) by RVSUM_1: 51

            .= (f . ((a * v1),(a * w1))) by A1

            .= (f . ((g . (a,v)),(a * w1))) by A3

            .= ((a * v) + (a * w)) by A3;

            hence (a1 * (v + w)) = ((a1 * v) + (a1 * w));

          end;

          hereby

            let a1,b1 be Real, v be VECTOR of RLSMS;

            reconsider a = a1, b = b1 as Real;

            reconsider v1 = v as Element of ( REAL n);

            reconsider v2 = v1 as Element of (n -tuples_on REAL );

            ((a + b) * v) = ((a + b) * v2) by A3

            .= ((a * v1) + (b * v1)) by RVSUM_1: 50

            .= (f . ((a * v1),(b * v1))) by A1

            .= (f . ((g . (a,v)),(b * v1))) by A3

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

            hence ((a1 + b1) * v) = ((a1 * v) + (b1 * v));

          end;

          hereby

            let a1,b1 be Real, v be VECTOR of RLSMS;

            reconsider a = a1, b = b1 as Real;

            reconsider v1 = v as Element of ( REAL n);

            reconsider v2 = v1 as Element of (n -tuples_on REAL );

            ((a * b) * v) = ((a * b) * v2) by A3

            .= (a * (b * v1)) by RVSUM_1: 49

            .= (g . (a,(b * v1))) by A3

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

            hence ((a1 * b1) * v) = (a1 * (b1 * v));

          end;

          hereby

            let v be VECTOR of RLSMS;

            reconsider v1 = v as Element of (n -tuples_on REAL );

            

            thus (1 * v) = (1 * v1) by A3

            .= v by RVSUM_1: 52;

          end;

        end;

         A14:

        now

          let a,b,c be VECTOR of RLSMS;

          reconsider a1 = a, b1 = b, c1 = c as Element of ( REAL n);

          thus ( dist (a,b)) = 0 implies a = b

          proof

            assume ( dist (a,b)) = 0 ;

            then (( Pitag_dist n) . (a,b)) = 0 by METRIC_1:def 1;

            then |.(a1 - b1).| = 0 by EUCLID:def 6;

            hence thesis by EUCLID: 16;

          end;

          

           A15: ( dist (a,c)) = (( Pitag_dist n) . (a,c)) by METRIC_1:def 1

          .= |.(a1 - c1).| by EUCLID:def 6;

           |.(a1 - a1).| = 0 ;

          then (( Pitag_dist n) . (a,a)) = 0 by EUCLID:def 6;

          hence ( dist (a,a)) = 0 by METRIC_1:def 1;

          

          thus ( dist (a,b)) = (( Pitag_dist n) . (a,b)) by METRIC_1:def 1

          .= |.(a1 - b1).| by EUCLID:def 6

          .= |.(b1 - a1).| by EUCLID: 18

          .= (( Pitag_dist n) . (b,a)) by EUCLID:def 6

          .= ( dist (b,a)) by METRIC_1:def 1;

          

           A16: ( dist (b,c)) = (( Pitag_dist n) . (b,c)) by METRIC_1:def 1

          .= |.(b1 - c1).| by EUCLID:def 6;

          ( dist (a,b)) = (( Pitag_dist n) . (a,b)) by METRIC_1:def 1

          .= |.(a1 - b1).| by EUCLID:def 6;

          hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A15, A16, EUCLID: 19;

        end;

        reconsider RLSMS as strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSMetrStruct by A5, A4, A6, A12, A13, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

        reconsider RLSMS as strict RealLinearMetrSpace by A14, A7, A10, Def5, Def6, METRIC_1: 1, METRIC_1: 2, METRIC_1: 3, METRIC_1: 4;

        take RLSMS;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

        let V1,V2 be strict RealLinearMetrSpace such that

         A17: the carrier of V1 = ( REAL n) and

         A18: the distance of V1 = ( Pitag_dist n) & ( 0. V1) = ( 0* n) and

         A19: for x,y be Element of ( REAL n) holds (the addF of V1 . (x,y)) = (x + y) and

         A20: for x be Element of ( REAL n), r be Element of REAL holds (the Mult of V1 . (r,x)) = (r * x) and

         A21: the carrier of V2 = ( REAL n) and

         A22: the distance of V2 = ( Pitag_dist n) & ( 0. V2) = ( 0* n) and

         A23: for x,y be Element of ( REAL n) holds (the addF of V2 . (x,y)) = (x + y) and

         A24: for x be Element of ( REAL n), r be Element of REAL holds (the Mult of V2 . (r,x)) = (r * x);

        now

          let x,y be Element of V1;

          reconsider x1 = x, y1 = y as Element of ( REAL n) by A17;

          

          thus (the addF of V1 . (x,y)) = (x1 + y1) by A19

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

        end;

        then

         A25: the addF of V1 = the addF of V2 by A17, A21, BINOP_1: 2;

        now

          let r be Element of REAL , x be Element of V1;

          reconsider x1 = x as Element of ( REAL n) by A17;

          

          thus (the Mult of V1 . (r,x)) = (r * x1) by A20

          .= (the Mult of V2 . (r,x)) by A24;

        end;

        hence thesis by A17, A18, A21, A22, A25, BINOP_1: 2;

      end;

    end

    theorem :: VECTMETR:9

    for n be Element of NAT holds for f be onto isometric Function of ( RLMSpace n), ( RLMSpace n) holds ( rng f) = ( REAL n)

    proof

      let n be Element of NAT ;

      let f be onto isometric Function of ( RLMSpace n), ( RLMSpace n);

      

      thus ( rng f) = the carrier of ( RLMSpace n) by FUNCT_2:def 3

      .= ( REAL n) by Def8;

    end;

    begin

    definition

      let n be Element of NAT ;

      :: VECTMETR:def9

      func IsomGroup n -> strict multMagma means

      : Def9: the carrier of it = ( ISOM ( RLMSpace n)) & for f,g be Function st f in ( ISOM ( RLMSpace n)) & g in ( ISOM ( RLMSpace n)) holds (the multF of it . (f,g)) = (f * g);

      existence

      proof

        defpred P[ set, set, set] means ex f,g be Function st f = $1 & g = $2 & $3 = (f * g);

        

         A1: for x,y be Element of ( ISOM ( RLMSpace n)) holds ex z be Element of ( ISOM ( RLMSpace n)) st P[x, y, z]

        proof

          let x,y be Element of ( ISOM ( RLMSpace n));

          reconsider x1 = x as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          reconsider y1 = y as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          reconsider z = (x1 * y1) as Element of ( ISOM ( RLMSpace n)) by Def4;

          take z;

          take x1, y1;

          thus thesis;

        end;

        consider o be BinOp of ( ISOM ( RLMSpace n)) such that

         A2: for a,b be Element of ( ISOM ( RLMSpace n)) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

        take G = multMagma (# ( ISOM ( RLMSpace n)), o #);

        for f,g be Function st f in ( ISOM ( RLMSpace n)) & g in ( ISOM ( RLMSpace n)) holds (the multF of G . (f,g)) = (f * g)

        proof

          let f,g be Function;

          assume f in ( ISOM ( RLMSpace n)) & g in ( ISOM ( RLMSpace n));

          then ex f1,g1 be Function st f1 = f & g1 = g & (o . (f,g)) = (f1 * g1) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set V = ( RLMSpace n);

        let G1,G2 be strict multMagma such that

         A3: the carrier of G1 = ( ISOM V) and

         A4: for f,g be Function st f in ( ISOM V) & g in ( ISOM V) holds (the multF of G1 . (f,g)) = (f * g) and

         A5: the carrier of G2 = ( ISOM V) and

         A6: for f,g be Function st f in ( ISOM V) & g in ( ISOM V) holds (the multF of G2 . (f,g)) = (f * g);

        now

          let f,g be Element of G1;

          reconsider f1 = f as Function of ( RLMSpace n), ( RLMSpace n) by A3, Def4;

          reconsider g1 = g as Function of ( RLMSpace n), ( RLMSpace n) by A3, Def4;

          

          thus (the multF of G1 . (f,g)) = (f1 * g1) by A3, A4

          .= (the multF of G2 . (f,g)) by A3, A6;

        end;

        hence thesis by A3, A5, BINOP_1: 2;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster ( IsomGroup n) -> non empty;

      coherence

      proof

        the carrier of ( IsomGroup n) = ( ISOM ( RLMSpace n)) by Def9;

        hence thesis;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster ( IsomGroup n) -> associative Group-like;

      coherence

      proof

        now

          let x,y,z be Element of ( IsomGroup n);

          x in the carrier of ( IsomGroup n);

          then

           A1: x in ( ISOM ( RLMSpace n)) by Def9;

          then

          reconsider x1 = x as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          y in the carrier of ( IsomGroup n);

          then

           A2: y in ( ISOM ( RLMSpace n)) by Def9;

          then

          reconsider y1 = y as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          

           A3: (x1 * y1) in ( ISOM ( RLMSpace n)) by Def4;

          z in the carrier of ( IsomGroup n);

          then

           A4: z in ( ISOM ( RLMSpace n)) by Def9;

          then

          reconsider z1 = z as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          

           A5: (y1 * z1) in ( ISOM ( RLMSpace n)) by Def4;

          

          thus ((x * y) * z) = (the multF of ( IsomGroup n) . ((x1 * y1),z)) by A1, A2, Def9

          .= ((x1 * y1) * z1) by A4, A3, Def9

          .= (x1 * (y1 * z1)) by RELAT_1: 36

          .= (the multF of ( IsomGroup n) . (x,(y1 * z1))) by A1, A5, Def9

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

        end;

        hence ( IsomGroup n) is associative by GROUP_1:def 3;

        ex e be Element of ( IsomGroup n) st for h be Element of ( IsomGroup n) holds (h * e) = h & (e * h) = h & ex g be Element of ( IsomGroup n) st (h * g) = e & (g * h) = e

        proof

          

           A6: ( id ( RLMSpace n)) in ( ISOM ( RLMSpace n)) by Def4;

          then

          reconsider e = ( id ( RLMSpace n)) as Element of ( IsomGroup n) by Def9;

          take e;

          let h be Element of ( IsomGroup n);

          h in the carrier of ( IsomGroup n);

          then

           A7: h in ( ISOM ( RLMSpace n)) by Def9;

          then

          reconsider h1 = h as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          

          thus (h * e) = (h1 * ( id the carrier of ( RLMSpace n))) by A6, A7, Def9

          .= h by FUNCT_2: 17;

          

          thus (e * h) = (( id the carrier of ( RLMSpace n)) * h1) by A6, A7, Def9

          .= h by FUNCT_2: 17;

          

           A8: ( rng h1) = ( [#] ( RLMSpace n)) by FUNCT_2:def 3;

          

           A9: (h1 " ) in ( ISOM ( RLMSpace n)) by Def4;

          then

          reconsider g = (h1 " ) as Element of ( IsomGroup n) by Def9;

          take g;

          

          thus (h * g) = (h1 * (h1 " )) by A7, A9, Def9

          .= e by A8, TOPS_2: 52;

          

          thus (g * h) = ((h1 " ) * h1) by A7, A9, Def9

          .= ( id ( dom h1)) by A8, TOPS_2: 52

          .= e by FUNCT_2:def 1;

        end;

        hence thesis by GROUP_1:def 2;

      end;

    end

    theorem :: VECTMETR:10

    

     Th7: for n be Element of NAT holds ( 1_ ( IsomGroup n)) = ( id ( RLMSpace n))

    proof

      let n be Element of NAT ;

      

       A1: ( id ( RLMSpace n)) in ( ISOM ( RLMSpace n)) by Def4;

      then

      reconsider e = ( id ( RLMSpace n)) as Element of ( IsomGroup n) by Def9;

      now

        let h be Element of ( IsomGroup n);

        h in the carrier of ( IsomGroup n);

        then

         A2: h in ( ISOM ( RLMSpace n)) by Def9;

        then

        reconsider h1 = h as Function of ( RLMSpace n), ( RLMSpace n) by Def4;

        

        thus (h * e) = (h1 * ( id the carrier of ( RLMSpace n))) by A1, A2, Def9

        .= h by FUNCT_2: 17;

        

        thus (e * h) = (( id the carrier of ( RLMSpace n)) * h1) by A1, A2, Def9

        .= h by FUNCT_2: 17;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: VECTMETR:11

    

     Th8: for n be Element of NAT holds for f be Element of ( IsomGroup n) holds for g be Function of ( RLMSpace n), ( RLMSpace n) st f = g holds (f " ) = (g " )

    proof

      let n be Element of NAT ;

      let f be Element of ( IsomGroup n);

      let g be Function of ( RLMSpace n), ( RLMSpace n);

      f in the carrier of ( IsomGroup n);

      then

       A1: f in ( ISOM ( RLMSpace n)) by Def9;

      then

      reconsider f1 = f as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

      assume

       A2: f = g;

      then f1 = g;

      then

       A3: (g " ) in ( ISOM ( RLMSpace n)) by Def4;

      then

      reconsider g1 = (g " ) as Element of ( IsomGroup n) by Def9;

      

       A4: ( rng f1) = ( [#] ( RLMSpace n)) by FUNCT_2:def 3;

      

       A5: (g1 * f) = ((g " ) * f1) by A1, A3, Def9

      .= ( id ( dom f1)) by A2, A4, TOPS_2: 52

      .= ( id ( RLMSpace n)) by FUNCT_2:def 1

      .= ( 1_ ( IsomGroup n)) by Th7;

      (f * g1) = (f1 * (g " )) by A1, A3, Def9

      .= ( id ( RLMSpace n)) by A2, A4, TOPS_2: 52

      .= ( 1_ ( IsomGroup n)) by Th7;

      hence thesis by A5, GROUP_1: 5;

    end;

    definition

      let n be Element of NAT ;

      let G be Subgroup of ( IsomGroup n);

      :: VECTMETR:def10

      func SubIsomGroupRel G -> Relation of the carrier of ( RLMSpace n) means

      : Def10: for A,B be Element of ( RLMSpace n) holds [A, B] in it iff ex f be Function st f in the carrier of G & (f . A) = B;

      existence

      proof

        defpred P[ object, object] means ex f be Function st f in the carrier of G & (f . $1) = $2;

        consider R be Relation of the carrier of ( RLMSpace n), the carrier of ( RLMSpace n) such that

         A1: for x,y be object holds [x, y] in R iff x in the carrier of ( RLMSpace n) & y in the carrier of ( RLMSpace n) & P[x, y] from RELSET_1:sch 1;

        take R;

        let A,B be Element of ( RLMSpace n);

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of the carrier of ( RLMSpace n) such that

         A2: for A,B be Element of ( RLMSpace n) holds [A, B] in R1 iff ex f be Function st f in the carrier of G & (f . A) = B and

         A3: for A,B be Element of ( RLMSpace n) holds [A, B] in R2 iff ex f be Function st f in the carrier of G & (f . A) = B;

        now

          let a,b be object;

          thus [a, b] in R1 implies [a, b] in R2

          proof

            assume

             A4: [a, b] in R1;

            then

            reconsider a1 = a, b1 = b as Element of ( RLMSpace n) by ZFMISC_1: 87;

            ex f be Function st f in the carrier of G & (f . a1) = b1 by A2, A4;

            hence thesis by A3;

          end;

          assume

           A5: [a, b] in R2;

          then

          reconsider a1 = a, b1 = b as Element of ( RLMSpace n) by ZFMISC_1: 87;

          ex f be Function st f in the carrier of G & (f . a1) = b1 by A3, A5;

          hence [a, b] in R1 by A2;

        end;

        hence R1 = R2 by RELAT_1:def 2;

      end;

    end

    registration

      let n be Element of NAT ;

      let G be Subgroup of ( IsomGroup n);

      cluster ( SubIsomGroupRel G) -> total symmetric transitive;

      coherence

      proof

        set S = ( SubIsomGroupRel G);

        set X = the carrier of ( RLMSpace n);

        now

          let x be object;

          assume x in X;

          then

          reconsider x1 = x as Element of ( RLMSpace n);

          ( 1_ ( IsomGroup n)) = ( id ( RLMSpace n)) by Th7;

          then ( id ( RLMSpace n)) in G by GROUP_2: 46;

          then

           A1: ( id ( RLMSpace n)) in the carrier of G;

          (( id ( RLMSpace n)) . x1) = x1;

          hence [x, x] in S by A1, Def10;

        end;

        then

         A2: S is_reflexive_in X by RELAT_2:def 1;

        then

         A3: ( field S) = X by ORDERS_1: 13;

        ( dom S) = X by A2, ORDERS_1: 13;

        hence S is total by PARTFUN1:def 2;

        now

          let x,y be object;

          assume that

           A4: x in X & y in X and

           A5: [x, y] in S;

          reconsider x1 = x, y1 = y as Element of ( RLMSpace n) by A4;

          consider f be Function such that

           A6: f in the carrier of G and

           A7: (f . x1) = y1 by A5, Def10;

          reconsider f1 = f as Element of G by A6;

          

           A8: the carrier of G c= the carrier of ( IsomGroup n) by GROUP_2:def 5;

          then

          reconsider f3 = f1 as Element of ( IsomGroup n);

          f in the carrier of ( IsomGroup n) by A6, A8;

          then f in ( ISOM ( RLMSpace n)) by Def9;

          then

          reconsider f2 = f as onto isometric Function of ( RLMSpace n), ( RLMSpace n) by Def4;

          x1 in the carrier of ( RLMSpace n);

          then x1 in ( dom f2) by FUNCT_2:def 1;

          then

           A9: ((f " ) . y1) = x1 by A7, FUNCT_1: 34;

          (f1 " ) = (f3 " ) by GROUP_2: 48

          .= (f2 " ) by Th8

          .= (f " ) by TOPS_2:def 4;

          hence [y, x] in S by A9, Def10;

        end;

        then S is_symmetric_in X by RELAT_2:def 3;

        hence S is symmetric by A3, RELAT_2:def 11;

        now

          let x,y,z be object;

          assume that

           A10: x in X & y in X & z in X and

           A11: [x, y] in S and

           A12: [y, z] in S;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( RLMSpace n) by A10;

          consider f be Function such that

           A13: f in the carrier of G and

           A14: (f . x1) = y1 by A11, Def10;

          reconsider f2 = f as Element of G by A13;

          

           A15: the carrier of G c= the carrier of ( IsomGroup n) by GROUP_2:def 5;

          then

          reconsider f3 = f2 as Element of ( IsomGroup n);

          f in the carrier of ( IsomGroup n) by A13, A15;

          then

           A16: f in ( ISOM ( RLMSpace n)) by Def9;

          consider g be Function such that

           A17: g in the carrier of G and

           A18: (g . y1) = z1 by A12, Def10;

          reconsider g2 = g as Element of G by A17;

          

           A19: x1 in the carrier of ( RLMSpace n);

          reconsider g3 = g2 as Element of ( IsomGroup n) by A15;

          f2 in G & g2 in G;

          then

           A20: (g3 * f3) in G by GROUP_2: 50;

          g in the carrier of ( IsomGroup n) by A17, A15;

          then g in ( ISOM ( RLMSpace n)) by Def9;

          then (g3 * f3) = (g * f) by A16, Def9;

          then

           A21: (g * f) in the carrier of G by A20;

          f is onto isometric Function of ( RLMSpace n), ( RLMSpace n) by A16, Def4;

          then x1 in ( dom f) by A19, FUNCT_2:def 1;

          then ((g * f) . x1) = z1 by A14, A18, FUNCT_1: 13;

          hence [x, z] in S by A21, Def10;

        end;

        then S is_transitive_in X by RELAT_2:def 8;

        hence thesis by A3, RELAT_2:def 16;

      end;

    end