topreal7.miz



    begin

    reserve i,j,n for Element of NAT ,

f,g,h,k for FinSequence of REAL ,

M,N for non empty MetrSpace;

    theorem :: TOPREAL7:1

    

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

    proof

      let a,b,c,d be Real;

      b <= ( max (a,b)) & d <= ( max (c,d)) by XXREAL_0: 25;

      then

       A1: (b + d) <= (( max (a,b)) + ( max (c,d))) by XREAL_1: 7;

      a <= ( max (a,b)) & c <= ( max (c,d)) by XXREAL_0: 25;

      then (a + c) <= (( max (a,b)) + ( max (c,d))) by XREAL_1: 7;

      hence thesis by A1, XXREAL_0: 28;

    end;

    theorem :: TOPREAL7:2

    

     Th2: for a,b,c,d,e,f be Real st a <= (b + c) & d <= (e + f) holds ( max (a,d)) <= (( max (b,e)) + ( max (c,f)))

    proof

      let a,b,c,d,e,f be Real;

      assume a <= (b + c) & d <= (e + f);

      then

       A1: ( max (a,d)) <= ( max ((b + c),(e + f))) by XXREAL_0: 26;

      ( max ((b + c),(e + f))) <= (( max (b,e)) + ( max (c,f))) by Th1;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: TOPREAL7:3

    for f,g be FinSequence holds ( dom g) c= ( dom (f ^ g))

    proof

      let f,g be FinSequence;

      ( len g) <= (( len f) + ( len g)) by NAT_1: 11;

      then ( Seg ( len g)) c= ( Seg (( len f) + ( len g))) by FINSEQ_1: 5;

      then ( dom g) c= ( Seg (( len f) + ( len g))) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 7;

    end;

    theorem :: TOPREAL7:4

    

     Th4: for i be Nat holds for f,g be FinSequence st ( len f) < i & i <= (( len f) + ( len g)) holds (i - ( len f)) in ( dom g)

    proof

      let i be Nat;

      let f,g be FinSequence such that

       A1: ( len f) < i and

       A2: i <= (( len f) + ( len g));

      

       A3: (i - ( len f)) is Element of NAT by A1, INT_1: 5;

      

       A4: (i - ( len f)) <= ((( len f) + ( len g)) - ( len f)) by A2, XREAL_1: 9;

      (i - ( len f)) > (( len f) - ( len f)) by A1, XREAL_1: 14;

      then 1 <= (i - ( len f)) by A3, NAT_1: 14;

      hence thesis by A3, A4, FINSEQ_3: 25;

    end;

    theorem :: TOPREAL7:5

    

     Th5: for f,g,h,k be FinSequence st (f ^ g) = (h ^ k) & ( len f) = ( len h) & ( len g) = ( len k) holds f = h & g = k

    proof

      let f,g,h,k be FinSequence such that

       A1: (f ^ g) = (h ^ k) and

       A2: ( len f) = ( len h) and

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

      

       A4: for i be Nat st 1 <= i & i <= ( len f) holds (f . i) = (h . i)

      proof

        let i be Nat;

        assume

         A5: 1 <= i & i <= ( len f);

        then

         A6: i in ( dom h) by A2, FINSEQ_3: 25;

        i in ( dom f) by A5, FINSEQ_3: 25;

        

        hence (f . i) = ((f ^ g) . i) by FINSEQ_1:def 7

        .= (h . i) by A1, A6, FINSEQ_1:def 7;

      end;

      for i be Nat st 1 <= i & i <= ( len g) holds (g . i) = (k . i)

      proof

        let i be Nat;

        assume

         A7: 1 <= i & i <= ( len g);

        then

         A8: i in ( dom k) by A3, FINSEQ_3: 25;

        i in ( dom g) by A7, FINSEQ_3: 25;

        

        hence (g . i) = ((f ^ g) . (( len f) + i)) by FINSEQ_1:def 7

        .= (k . i) by A1, A2, A8, FINSEQ_1:def 7;

      end;

      hence thesis by A2, A3, A4, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:6

    

     Th6: ( len f) = ( len g) or ( dom f) = ( dom g) implies ( len (f + g)) = ( len f) & ( dom (f + g)) = ( dom f)

    proof

      reconsider f1 = f as Element of (( len f) -tuples_on REAL ) by FINSEQ_2: 92;

      assume ( len f) = ( len g) or ( dom f) = ( dom g);

      then ( len f) = ( len g) by FINSEQ_3: 29;

      then

      reconsider g1 = g as Element of (( len f) -tuples_on REAL ) by FINSEQ_2: 92;

      (f1 + g1) is Element of (( len f) -tuples_on REAL );

      hence ( len (f + g)) = ( len f) by CARD_1:def 7;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: TOPREAL7:7

    

     Th7: ( len f) = ( len g) or ( dom f) = ( dom g) implies ( len (f - g)) = ( len f) & ( dom (f - g)) = ( dom f)

    proof

      reconsider f1 = f as Element of (( len f) -tuples_on REAL ) by FINSEQ_2: 92;

      assume ( len f) = ( len g) or ( dom f) = ( dom g);

      then ( len f) = ( len g) by FINSEQ_3: 29;

      then

      reconsider g1 = g as Element of (( len f) -tuples_on REAL ) by FINSEQ_2: 92;

      (f1 - g1) is Element of (( len f) -tuples_on REAL );

      hence ( len (f - g)) = ( len f) by CARD_1:def 7;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: TOPREAL7:8

    

     Th8: ( len f) = ( len ( sqr f)) & ( dom f) = ( dom ( sqr f)) by RVSUM_1: 143;

    theorem :: TOPREAL7:9

    

     Th9: ( len f) = ( len ( abs f)) & ( dom f) = ( dom ( abs f))

    proof

      ( rng f) c= REAL & ( dom absreal ) = REAL by FUNCT_2:def 1;

      hence ( len f) = ( len ( abs f)) by FINSEQ_2: 29;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: TOPREAL7:10

    

     Th10: ( sqr (f ^ g)) = (( sqr f) ^ ( sqr g)) by RVSUM_1: 144;

    theorem :: TOPREAL7:11

    ( abs (f ^ g)) = (( abs f) ^ ( abs g))

    proof

      

       A1: ( len g) = ( len ( abs g)) & ( len (f ^ g)) = (( len f) + ( len g)) by Th9, FINSEQ_1: 22;

      

       A2: ( len ( abs (f ^ g))) = ( len (f ^ g)) by Th9;

      

       A3: ( len f) = ( len ( abs f)) by Th9;

      

       A4: for i be Nat st 1 <= i & i <= ( len ( abs (f ^ g))) holds (( abs (f ^ g)) . i) = ((( abs f) ^ ( abs g)) . i)

      proof

        let i be Nat;

        assume that

         A5: 1 <= i and

         A6: i <= ( len ( abs (f ^ g)));

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

        

         A7: i in ( dom (f ^ g)) by A2, A5, A6, FINSEQ_3: 25;

        per cases ;

          suppose

           A8: i in ( dom f);

          then

           A9: i in ( dom ( abs f)) by Th9;

          

          thus (( abs (f ^ g)) . i) = ( absreal . ((f ^ g) . i)) by A7, FUNCT_1: 13

          .= ( absreal . (f . i)) by A8, FINSEQ_1:def 7

          .= |.(f . i1).| by EUCLID:def 2

          .= (( abs f) . i1) by A9, TOPREAL6: 12

          .= ((( abs f) ^ ( abs g)) . i) by A9, FINSEQ_1:def 7;

        end;

          suppose not i in ( dom f);

          then

           A10: ( len f) < i by A5, FINSEQ_3: 25;

          then

          reconsider j = (i1 - ( len f)) as Element of NAT by INT_1: 5;

          

           A11: i <= ( len (f ^ g)) by A6, Th9;

          then

           A12: j in ( dom ( abs g)) by A1, A10, Th4;

          

           A13: i <= ( len (( abs f) ^ ( abs g))) by A3, A1, A2, A6, FINSEQ_1: 22;

          

          thus (( abs (f ^ g)) . i) = ( absreal . ((f ^ g) . i)) by A7, FUNCT_1: 13

          .= ( absreal . (g . j)) by A10, A11, FINSEQ_1: 24

          .= |.(g . j).| by EUCLID:def 2

          .= (( abs g) . j) by A12, TOPREAL6: 12

          .= ((( abs f) ^ ( abs g)) . i) by A3, A10, A13, FINSEQ_1: 24;

        end;

      end;

      ( len ( abs (f ^ g))) = ( len (( abs f) ^ ( abs g))) by A3, A1, A2, FINSEQ_1: 22;

      hence thesis by A4, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:12

    ( len f) = ( len h) & ( len g) = ( len k) implies ( sqr ((f ^ g) + (h ^ k))) = (( sqr (f + h)) ^ ( sqr (g + k)))

    proof

      assume that

       A1: ( len f) = ( len h) and

       A2: ( len g) = ( len k);

      

       A3: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      

       A4: ( len (h ^ k)) = (( len h) + ( len k)) by FINSEQ_1: 22;

      

       A5: ( len ( sqr ((f ^ g) + (h ^ k)))) = ( len ((f ^ g) + (h ^ k))) by Th8

      .= ( len (f ^ g)) by A1, A2, A3, A4, Th6

      .= (( len (f + h)) + ( len g)) by A1, A3, Th6

      .= (( len (f + h)) + ( len (g + k))) by A2, Th6

      .= (( len ( sqr (f + h))) + ( len (g + k))) by Th8

      .= (( len ( sqr (f + h))) + ( len ( sqr (g + k)))) by Th8

      .= ( len (( sqr (f + h)) ^ ( sqr (g + k)))) by FINSEQ_1: 22;

      for i be Nat st 1 <= i & i <= ( len ( sqr ((f ^ g) + (h ^ k)))) holds (( sqr ((f ^ g) + (h ^ k))) . i) = ((( sqr (f + h)) ^ ( sqr (g + k))) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ( sqr ((f ^ g) + (h ^ k))));

        i in ( dom ( sqr ((f ^ g) + (h ^ k)))) by A6, A7, FINSEQ_3: 25;

        then

         A8: i in ( dom ((f ^ g) + (h ^ k))) by Th8;

        per cases ;

          suppose

           A9: i in ( dom f);

          then

           A10: i in ( dom (f + h)) by A1, Th6;

          then

           A11: i in ( dom ( sqr (f + h))) by Th8;

          

           A12: i in ( dom h) by A1, A9, FINSEQ_3: 29;

          

          thus (( sqr ((f ^ g) + (h ^ k))) . i) = ((((f ^ g) + (h ^ k)) . i) ^2 ) by VALUED_1: 11

          .= ((((f ^ g) . i) + ((h ^ k) . i)) ^2 ) by A8, VALUED_1:def 1

          .= (((f . i) + ((h ^ k) . i)) ^2 ) by A9, FINSEQ_1:def 7

          .= (((f . i) + (h . i)) ^2 ) by A12, FINSEQ_1:def 7

          .= (((f + h) . i) ^2 ) by A10, VALUED_1:def 1

          .= (( sqr (f + h)) . i) by VALUED_1: 11

          .= ((( sqr (f + h)) ^ ( sqr (g + k))) . i) by A11, FINSEQ_1:def 7;

        end;

          suppose not i in ( dom f);

          then

           A13: ( len f) < i by A6, FINSEQ_3: 25;

          then

          reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

          

           A14: ( len (f + h)) < i by A1, A13, Th6;

          then

           A15: ( len ( sqr (f + h))) < i by Th8;

          i <= ( len ((f ^ g) + (h ^ k))) by A7, Th8;

          then

           A16: i <= ( len (f ^ g)) by A1, A2, A3, A4, Th6;

          then i <= (( len (f + h)) + ( len g)) by A1, A3, Th6;

          then i <= (( len (f + h)) + ( len (g + k))) by A2, Th6;

          then (i - ( len (f + h))) in ( dom (g + k)) by A14, Th4;

          then

           A17: j in ( dom (g + k)) by A1, Th6;

          ( len f) = ( len (f + h)) by A1, Th6;

          then

           A18: j = (i - ( len ( sqr (f + h)))) by Th8;

          

          thus (( sqr ((f ^ g) + (h ^ k))) . i) = ((((f ^ g) + (h ^ k)) . i) ^2 ) by VALUED_1: 11

          .= ((((f ^ g) . i) + ((h ^ k) . i)) ^2 ) by A8, VALUED_1:def 1

          .= (((g . j) + ((h ^ k) . i)) ^2 ) by A13, A16, FINSEQ_1: 24

          .= (((g . j) + (k . j)) ^2 ) by A1, A2, A3, A4, A13, A16, FINSEQ_1: 24

          .= (((g + k) . j) ^2 ) by A17, VALUED_1:def 1

          .= (( sqr (g + k)) . j) by VALUED_1: 11

          .= ((( sqr (f + h)) ^ ( sqr (g + k))) . i) by A5, A7, A15, A18, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:13

    ( len f) = ( len h) & ( len g) = ( len k) implies ( abs ((f ^ g) + (h ^ k))) = (( abs (f + h)) ^ ( abs (g + k)))

    proof

      assume that

       A1: ( len f) = ( len h) and

       A2: ( len g) = ( len k);

      

       A3: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      

       A4: ( len (h ^ k)) = (( len h) + ( len k)) by FINSEQ_1: 22;

      

       A5: ( len ( abs ((f ^ g) + (h ^ k)))) = ( len ((f ^ g) + (h ^ k))) by Th9

      .= ( len (f ^ g)) by A1, A2, A3, A4, Th6

      .= (( len (f + h)) + ( len g)) by A1, A3, Th6

      .= (( len (f + h)) + ( len (g + k))) by A2, Th6

      .= (( len ( abs (f + h))) + ( len (g + k))) by Th9

      .= (( len ( abs (f + h))) + ( len ( abs (g + k)))) by Th9

      .= ( len (( abs (f + h)) ^ ( abs (g + k)))) by FINSEQ_1: 22;

      for i be Nat st 1 <= i & i <= ( len ( abs ((f ^ g) + (h ^ k)))) holds (( abs ((f ^ g) + (h ^ k))) . i) = ((( abs (f + h)) ^ ( abs (g + k))) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ( abs ((f ^ g) + (h ^ k))));

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

        

         A8: i in ( dom ( abs ((f ^ g) + (h ^ k)))) by A6, A7, FINSEQ_3: 25;

        then

         A9: i in ( dom ((f ^ g) + (h ^ k))) by Th9;

        per cases ;

          suppose

           A10: i in ( dom f);

          then

           A11: i in ( dom h) by A1, FINSEQ_3: 29;

          

           A12: i in ( dom (f + h)) by A1, A10, Th6;

          then

           A13: i in ( dom ( abs (f + h))) by Th9;

          

          thus (( abs ((f ^ g) + (h ^ k))) . i) = |.(((f ^ g) + (h ^ k)) . i1).| by A8, TOPREAL6: 12

          .= |.(((f ^ g) . i) + ((h ^ k) . i)).| by A9, VALUED_1:def 1

          .= |.((f . i) + ((h ^ k) . i)).| by A10, FINSEQ_1:def 7

          .= |.((f . i) + (h . i)).| by A11, FINSEQ_1:def 7

          .= |.((f + h) . i1).| by A12, VALUED_1:def 1

          .= (( abs (f + h)) . i1) by A13, TOPREAL6: 12

          .= ((( abs (f + h)) ^ ( abs (g + k))) . i) by A13, FINSEQ_1:def 7;

        end;

          suppose not i in ( dom f);

          then

           A14: ( len f) < i by A6, FINSEQ_3: 25;

          then

          reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

          

           A15: ( len (f + h)) < i by A1, A14, Th6;

          then

           A16: ( len ( abs (f + h))) < i by Th9;

          i <= ( len ((f ^ g) + (h ^ k))) by A7, Th9;

          then

           A17: i <= ( len (f ^ g)) by A1, A2, A3, A4, Th6;

          then i <= (( len (f + h)) + ( len g)) by A1, A3, Th6;

          then i <= (( len (f + h)) + ( len (g + k))) by A2, Th6;

          then (i - ( len (f + h))) in ( dom (g + k)) by A15, Th4;

          then

           A18: j in ( dom (g + k)) by A1, Th6;

          then

           A19: j in ( dom ( abs (g + k))) by Th9;

          ( len f) = ( len (f + h)) by A1, Th6;

          then

           A20: j = (i - ( len ( abs (f + h)))) by Th9;

          

          thus (( abs ((f ^ g) + (h ^ k))) . i) = |.(((f ^ g) + (h ^ k)) . i1).| by A8, TOPREAL6: 12

          .= |.(((f ^ g) . i) + ((h ^ k) . i)).| by A9, VALUED_1:def 1

          .= |.((g . j) + ((h ^ k) . i)).| by A14, A17, FINSEQ_1: 24

          .= |.((g . j) + (k . j)).| by A1, A2, A3, A4, A14, A17, FINSEQ_1: 24

          .= |.((g + k) . j).| by A18, VALUED_1:def 1

          .= (( abs (g + k)) . j) by A19, TOPREAL6: 12

          .= ((( abs (f + h)) ^ ( abs (g + k))) . i) by A5, A7, A16, A20, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:14

    ( len f) = ( len h) & ( len g) = ( len k) implies ( sqr ((f ^ g) - (h ^ k))) = (( sqr (f - h)) ^ ( sqr (g - k)))

    proof

      assume that

       A1: ( len f) = ( len h) and

       A2: ( len g) = ( len k);

      

       A3: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      

       A4: ( len (h ^ k)) = (( len h) + ( len k)) by FINSEQ_1: 22;

      

       A5: ( len ( sqr ((f ^ g) - (h ^ k)))) = ( len ((f ^ g) - (h ^ k))) by Th8

      .= ( len (f ^ g)) by A1, A2, A3, A4, Th7

      .= (( len (f - h)) + ( len g)) by A1, A3, Th7

      .= (( len (f - h)) + ( len (g - k))) by A2, Th7

      .= (( len ( sqr (f - h))) + ( len (g - k))) by Th8

      .= (( len ( sqr (f - h))) + ( len ( sqr (g - k)))) by Th8

      .= ( len (( sqr (f - h)) ^ ( sqr (g - k)))) by FINSEQ_1: 22;

      for i be Nat st 1 <= i & i <= ( len ( sqr ((f ^ g) - (h ^ k)))) holds (( sqr ((f ^ g) - (h ^ k))) . i) = ((( sqr (f - h)) ^ ( sqr (g - k))) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ( sqr ((f ^ g) - (h ^ k))));

        i in ( dom ( sqr ((f ^ g) - (h ^ k)))) by A6, A7, FINSEQ_3: 25;

        then

         A8: i in ( dom ((f ^ g) - (h ^ k))) by Th8;

        per cases ;

          suppose

           A9: i in ( dom f);

          then

           A10: i in ( dom (f - h)) by A1, Th7;

          then

           A11: i in ( dom ( sqr (f - h))) by Th8;

          

           A12: i in ( dom h) by A1, A9, FINSEQ_3: 29;

          

          thus (( sqr ((f ^ g) - (h ^ k))) . i) = ((((f ^ g) - (h ^ k)) . i) ^2 ) by VALUED_1: 11

          .= ((((f ^ g) . i) - ((h ^ k) . i)) ^2 ) by A8, VALUED_1: 13

          .= (((f . i) - ((h ^ k) . i)) ^2 ) by A9, FINSEQ_1:def 7

          .= (((f . i) - (h . i)) ^2 ) by A12, FINSEQ_1:def 7

          .= (((f - h) . i) ^2 ) by A10, VALUED_1: 13

          .= (( sqr (f - h)) . i) by VALUED_1: 11

          .= ((( sqr (f - h)) ^ ( sqr (g - k))) . i) by A11, FINSEQ_1:def 7;

        end;

          suppose not i in ( dom f);

          then

           A13: ( len f) < i by A6, FINSEQ_3: 25;

          then

          reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

          

           A14: ( len (f - h)) < i by A1, A13, Th7;

          then

           A15: ( len ( sqr (f - h))) < i by Th8;

          i <= ( len ((f ^ g) - (h ^ k))) by A7, Th8;

          then

           A16: i <= ( len (f ^ g)) by A1, A2, A3, A4, Th7;

          then i <= (( len (f - h)) + ( len g)) by A1, A3, Th7;

          then i <= (( len (f - h)) + ( len (g - k))) by A2, Th7;

          then (i - ( len (f - h))) in ( dom (g - k)) by A14, Th4;

          then

           A17: j in ( dom (g - k)) by A1, Th7;

          ( len f) = ( len (f - h)) by A1, Th7;

          then

           A18: j = (i - ( len ( sqr (f - h)))) by Th8;

          

          thus (( sqr ((f ^ g) - (h ^ k))) . i) = ((((f ^ g) - (h ^ k)) . i) ^2 ) by VALUED_1: 11

          .= ((((f ^ g) . i) - ((h ^ k) . i)) ^2 ) by A8, VALUED_1: 13

          .= (((g . j) - ((h ^ k) . i)) ^2 ) by A13, A16, FINSEQ_1: 24

          .= (((g . j) - (k . j)) ^2 ) by A1, A2, A3, A4, A13, A16, FINSEQ_1: 24

          .= (((g - k) . j) ^2 ) by A17, VALUED_1: 13

          .= (( sqr (g - k)) . j) by VALUED_1: 11

          .= ((( sqr (f - h)) ^ ( sqr (g - k))) . i) by A5, A7, A15, A18, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:15

    

     Th15: ( len f) = ( len h) & ( len g) = ( len k) implies ( abs ((f ^ g) - (h ^ k))) = (( abs (f - h)) ^ ( abs (g - k)))

    proof

      assume that

       A1: ( len f) = ( len h) and

       A2: ( len g) = ( len k);

      

       A3: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      

       A4: ( len (h ^ k)) = (( len h) + ( len k)) by FINSEQ_1: 22;

      

       A5: ( len ( abs ((f ^ g) - (h ^ k)))) = ( len ((f ^ g) - (h ^ k))) by Th9

      .= ( len (f ^ g)) by A1, A2, A3, A4, Th7

      .= (( len (f - h)) + ( len g)) by A1, A3, Th7

      .= (( len (f - h)) + ( len (g - k))) by A2, Th7

      .= (( len ( abs (f - h))) + ( len (g - k))) by Th9

      .= (( len ( abs (f - h))) + ( len ( abs (g - k)))) by Th9

      .= ( len (( abs (f - h)) ^ ( abs (g - k)))) by FINSEQ_1: 22;

      for i be Nat st 1 <= i & i <= ( len ( abs ((f ^ g) - (h ^ k)))) holds (( abs ((f ^ g) - (h ^ k))) . i) = ((( abs (f - h)) ^ ( abs (g - k))) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ( abs ((f ^ g) - (h ^ k))));

        

         A8: i in ( dom ( abs ((f ^ g) - (h ^ k)))) by A6, A7, FINSEQ_3: 25;

        then

         A9: i in ( dom ((f ^ g) - (h ^ k))) by Th9;

        per cases ;

          suppose

           A10: i in ( dom f);

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

          

           A11: i in ( dom h) by A1, A10, FINSEQ_3: 29;

          

           A12: i in ( dom (f - h)) by A1, A10, Th7;

          then

           A13: i in ( dom ( abs (f - h))) by Th9;

          

          thus (( abs ((f ^ g) - (h ^ k))) . i) = |.(((f ^ g) - (h ^ k)) . i1).| by A8, TOPREAL6: 12

          .= |.(((f ^ g) . i) - ((h ^ k) . i)).| by A9, VALUED_1: 13

          .= |.((f . i) - ((h ^ k) . i)).| by A10, FINSEQ_1:def 7

          .= |.((f . i) - (h . i)).| by A11, FINSEQ_1:def 7

          .= |.((f - h) . i1).| by A12, VALUED_1: 13

          .= (( abs (f - h)) . i1) by A13, TOPREAL6: 12

          .= ((( abs (f - h)) ^ ( abs (g - k))) . i) by A13, FINSEQ_1:def 7;

        end;

          suppose

           A14: not i in ( dom f);

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

          

           A15: ( len f) < i by A6, A14, FINSEQ_3: 25;

          then

          reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

          

           A16: ( len (f - h)) < i by A1, A15, Th7;

          then

           A17: ( len ( abs (f - h))) < i by Th9;

          i <= ( len ((f ^ g) - (h ^ k))) by A7, Th9;

          then

           A18: i <= ( len (f ^ g)) by A1, A2, A3, A4, Th7;

          then i <= (( len (f - h)) + ( len g)) by A1, A3, Th7;

          then i <= (( len (f - h)) + ( len (g - k))) by A2, Th7;

          then (i - ( len (f - h))) in ( dom (g - k)) by A16, Th4;

          then

           A19: j in ( dom (g - k)) by A1, Th7;

          then

           A20: j in ( dom ( abs (g - k))) by Th9;

          ( len f) = ( len (f - h)) by A1, Th7;

          then

           A21: j = (i - ( len ( abs (f - h)))) by Th9;

          

          thus (( abs ((f ^ g) - (h ^ k))) . i) = |.(((f ^ g) - (h ^ k)) . i1).| by A8, TOPREAL6: 12

          .= |.(((f ^ g) . i) - ((h ^ k) . i)).| by A9, VALUED_1: 13

          .= |.((g . j) - ((h ^ k) . i)).| by A15, A18, FINSEQ_1: 24

          .= |.((g . j) - (k . j)).| by A1, A2, A3, A4, A15, A18, FINSEQ_1: 24

          .= |.((g - k) . j).| by A19, VALUED_1: 13

          .= (( abs (g - k)) . j) by A20, TOPREAL6: 12

          .= ((( abs (f - h)) ^ ( abs (g - k))) . i) by A5, A7, A17, A21, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: TOPREAL7:16

    

     Th16: ( len f) = n implies f in the carrier of ( Euclid n) by TOPREAL3: 45;

    theorem :: TOPREAL7:17

    ( len f) = n implies f in the carrier of ( TOP-REAL n) by TOPREAL3: 46;

    definition

      let M,N be non empty MetrStruct;

      :: TOPREAL7:def1

      func max-Prod2 (M,N) -> strict MetrStruct means

      : Def1: the carrier of it = [:the carrier of M, the carrier of N:] & for x,y be Point of it holds ex x1,y1 be Point of M, x2,y2 be Point of N st x = [x1, x2] & y = [y1, y2] & (the distance of it . (x,y)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2))));

      existence

      proof

        defpred P[ set, set, set] means ex x1,y1 be Point of M, x2,y2 be Point of N st $1 = [x1, x2] & $2 = [y1, y2] & $3 = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2))));

        set C = [:the carrier of M, the carrier of N:];

        

         A1: for x,y be Element of C holds ex u be Element of REAL st P[x, y, u]

        proof

          let x,y be Element of C;

          set x1 = (x `1 ), x2 = (x `2 ), y1 = (y `1 ), y2 = (y `2 );

          set m = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2))));

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

          take m;

          take x1, y1, x2, y2;

          thus thesis by MCART_1: 21;

        end;

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

         A2: for x,y be Element of C holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        take E = MetrStruct (# C, f #);

        thus the carrier of E = [:the carrier of M, the carrier of N:];

        let x,y be Point of E;

        consider x1,y1 be Point of M, x2,y2 be Point of N such that

         A3: x = [x1, x2] & y = [y1, y2] & (f . (x,y)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by A2;

        take x1, y1, x2, y2;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let A,B be strict MetrStruct such that

         A4: the carrier of A = [:the carrier of M, the carrier of N:] and

         A5: for x,y be Point of A holds ex x1,y1 be Point of M, x2,y2 be Point of N st x = [x1, x2] & y = [y1, y2] & (the distance of A . (x,y)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) and

         A6: the carrier of B = [:the carrier of M, the carrier of N:] and

         A7: for x,y be Point of B holds ex x1,y1 be Point of M, x2,y2 be Point of N st x = [x1, x2] & y = [y1, y2] & (the distance of B . (x,y)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2))));

        set f = the distance of A, g = the distance of B;

        for a,b be set st a in the carrier of A & b in the carrier of A holds (f . (a,b)) = (g . (a,b))

        proof

          let a,b be set;

          assume

           A8: a in the carrier of A & b in the carrier of A;

          then

          consider x1,y1 be Point of M, x2,y2 be Point of N such that

           A9: a = [x1, x2] and

           A10: b = [y1, y2] and

           A11: (f . (a,b)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by A5;

          consider m1,n1 be Point of M, m2,n2 be Point of N such that

           A12: a = [m1, m2] and

           A13: b = [n1, n2] and

           A14: (g . (a,b)) = ( max ((the distance of M . (m1,n1)),(the distance of N . (m2,n2)))) by A4, A6, A7, A8;

          

           A15: y1 = n1 by A10, A13, XTUPLE_0: 1;

          x1 = m1 & x2 = m2 by A9, A12, XTUPLE_0: 1;

          hence thesis by A10, A11, A13, A14, A15, XTUPLE_0: 1;

        end;

        hence thesis by A4, A6, BINOP_1: 1;

      end;

    end

    registration

      let M,N be non empty MetrStruct;

      cluster ( max-Prod2 (M,N)) -> non empty;

      coherence

      proof

        the carrier of ( max-Prod2 (M,N)) = [:the carrier of M, the carrier of N:] by Def1;

        hence the carrier of ( max-Prod2 (M,N)) is non empty;

      end;

    end

    definition

      let M,N be non empty MetrStruct, x be Point of M, y be Point of N;

      :: original: [

      redefine

      func [x,y] -> Element of ( max-Prod2 (M,N)) ;

      coherence

      proof

         [x, y] is Element of ( max-Prod2 (M,N)) by Def1;

        hence thesis;

      end;

    end

    definition

      let M,N be non empty MetrStruct, x be Point of ( max-Prod2 (M,N));

      :: original: `1

      redefine

      func x `1 -> Element of M ;

      coherence

      proof

        the carrier of ( max-Prod2 (M,N)) = [:the carrier of M, the carrier of N:] by Def1;

        hence thesis by MCART_1: 10;

      end;

      :: original: `2

      redefine

      func x `2 -> Element of N ;

      coherence

      proof

        the carrier of ( max-Prod2 (M,N)) = [:the carrier of M, the carrier of N:] by Def1;

        hence thesis by MCART_1: 10;

      end;

    end

    theorem :: TOPREAL7:18

    

     Th18: for M,N be non empty MetrStruct, m1,m2 be Point of M, n1,n2 be Point of N holds ( dist ( [m1, n1], [m2, n2])) = ( max (( dist (m1,m2)),( dist (n1,n2))))

    proof

      let M,N be non empty MetrStruct, m1,m2 be Point of M, n1,n2 be Point of N;

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A1: [m1, n1] = [x1, x2] and

       A2: [m2, n2] = [y1, y2] and

       A3: (the distance of ( max-Prod2 (M,N)) . ( [m1, n1], [m2, n2])) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

      

       A4: m2 = y1 by A2, XTUPLE_0: 1;

      m1 = x1 & n1 = x2 by A1, XTUPLE_0: 1;

      hence thesis by A2, A3, A4, XTUPLE_0: 1;

    end;

    theorem :: TOPREAL7:19

    for M,N be non empty MetrStruct, m,n be Point of ( max-Prod2 (M,N)) holds ( dist (m,n)) = ( max (( dist ((m `1 ),(n `1 ))),( dist ((m `2 ),(n `2 )))))

    proof

      let M,N be non empty MetrStruct, m,n be Point of ( max-Prod2 (M,N));

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A1: m = [x1, x2] and

       A2: n = [y1, y2] and

       A3: (the distance of ( max-Prod2 (M,N)) . (m,n)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

      

       A4: (m `2 ) = x2 by A1;

      (m `1 ) = x1 & (n `1 ) = y1 by A1, A2;

      hence thesis by A2, A3, A4;

    end;

    theorem :: TOPREAL7:20

    

     Th20: for M,N be Reflexive non empty MetrStruct holds ( max-Prod2 (M,N)) is Reflexive

    proof

      let M,N be Reflexive non empty MetrStruct;

      let a be Element of ( max-Prod2 (M,N));

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A1: a = [x1, x2] & a = [y1, y2] and

       A2: (the distance of ( max-Prod2 (M,N)) . (a,a)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

      the distance of M is Reflexive by METRIC_1:def 6;

      then

       A3: (the distance of M . (x1,x1)) = 0 ;

      the distance of N is Reflexive by METRIC_1:def 6;

      then

       A4: (the distance of N . (x2,x2)) = 0 ;

      x1 = y1 & x2 = y2 by A1, XTUPLE_0: 1;

      hence thesis by A2, A3, A4;

    end;

    registration

      let M,N be Reflexive non empty MetrStruct;

      cluster ( max-Prod2 (M,N)) -> Reflexive;

      coherence by Th20;

    end

    

     Lm1: for M,N be non empty MetrSpace holds ( max-Prod2 (M,N)) is discerning

    proof

      let M,N be non empty MetrSpace;

      let a,b be Element of ( max-Prod2 (M,N));

      assume

       A1: (the distance of ( max-Prod2 (M,N)) . (a,b)) = 0 ;

      

       A2: the distance of M is discerning by METRIC_1:def 7;

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A3: a = [x1, x2] & b = [y1, y2] and

       A4: (the distance of ( max-Prod2 (M,N)) . (a,b)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

       0 <= ( dist (x1,y1)) by METRIC_1: 5;

      then (the distance of M . (x1,y1)) = 0 by A1, A4, XXREAL_0: 49;

      then

       A5: the distance of N is discerning & x1 = y1 by A2, METRIC_1:def 7;

       0 <= ( dist (x2,y2)) by METRIC_1: 5;

      then (the distance of N . (x2,y2)) = 0 by A1, A4, XXREAL_0: 49;

      hence thesis by A3, A5;

    end;

    theorem :: TOPREAL7:21

    

     Th21: for M,N be symmetric non empty MetrStruct holds ( max-Prod2 (M,N)) is symmetric

    proof

      let M,N be symmetric non empty MetrStruct;

      let a,b be Element of ( max-Prod2 (M,N));

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A1: a = [x1, x2] and

       A2: b = [y1, y2] and

       A3: (the distance of ( max-Prod2 (M,N)) . (a,b)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

      consider m1,n1 be Point of M, m2,n2 be Point of N such that

       A4: b = [m1, m2] and

       A5: a = [n1, n2] and

       A6: (the distance of ( max-Prod2 (M,N)) . (b,a)) = ( max ((the distance of M . (m1,n1)),(the distance of N . (m2,n2)))) by Def1;

      

       A7: x1 = n1 by A1, A5, XTUPLE_0: 1;

      the distance of N is symmetric by METRIC_1:def 8;

      then

       A8: (the distance of N . (x2,y2)) = (the distance of N . (y2,x2));

      the distance of M is symmetric by METRIC_1:def 8;

      then

       A9: (the distance of M . (x1,y1)) = (the distance of M . (y1,x1));

      y1 = m1 & y2 = m2 by A2, A4, XTUPLE_0: 1;

      hence thesis by A1, A3, A5, A6, A9, A8, A7, XTUPLE_0: 1;

    end;

    registration

      let M,N be symmetric non empty MetrStruct;

      cluster ( max-Prod2 (M,N)) -> symmetric;

      coherence by Th21;

    end

    theorem :: TOPREAL7:22

    

     Th22: for M,N be triangle non empty MetrStruct holds ( max-Prod2 (M,N)) is triangle

    proof

      let M,N be triangle non empty MetrStruct;

      let a,b,c be Element of ( max-Prod2 (M,N));

      consider x1,y1 be Point of M, x2,y2 be Point of N such that

       A1: a = [x1, x2] and

       A2: b = [y1, y2] and

       A3: (the distance of ( max-Prod2 (M,N)) . (a,b)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

      consider m1,n1 be Point of M, m2,n2 be Point of N such that

       A4: b = [m1, m2] and

       A5: c = [n1, n2] and

       A6: (the distance of ( max-Prod2 (M,N)) . (b,c)) = ( max ((the distance of M . (m1,n1)),(the distance of N . (m2,n2)))) by Def1;

      

       A7: y1 = m1 & y2 = m2 by A2, A4, XTUPLE_0: 1;

      consider p1,q1 be Point of M, p2,q2 be Point of N such that

       A8: a = [p1, p2] and

       A9: c = [q1, q2] and

       A10: (the distance of ( max-Prod2 (M,N)) . (a,c)) = ( max ((the distance of M . (p1,q1)),(the distance of N . (p2,q2)))) by Def1;

      

       A11: q1 = n1 & q2 = n2 by A5, A9, XTUPLE_0: 1;

      the distance of N is triangle by METRIC_1:def 9;

      then

       A12: (the distance of N . (p2,q2)) <= ((the distance of N . (p2,y2)) + (the distance of N . (y2,q2)));

      the distance of M is triangle by METRIC_1:def 9;

      then

       A13: (the distance of M . (p1,q1)) <= ((the distance of M . (p1,y1)) + (the distance of M . (y1,q1)));

      x1 = p1 & x2 = p2 by A1, A8, XTUPLE_0: 1;

      hence thesis by A3, A6, A10, A13, A12, A7, A11, Th2;

    end;

    registration

      let M,N be triangle non empty MetrStruct;

      cluster ( max-Prod2 (M,N)) -> triangle;

      coherence by Th22;

    end

    registration

      let M,N be non empty MetrSpace;

      cluster ( max-Prod2 (M,N)) -> discerning;

      coherence by Lm1;

    end

    theorem :: TOPREAL7:23

    

     Th23: [:( TopSpaceMetr M), ( TopSpaceMetr N):] = ( TopSpaceMetr ( max-Prod2 (M,N)))

    proof

      set S = ( TopSpaceMetr M), T = ( TopSpaceMetr N);

      

       A1: ( TopSpaceMetr ( max-Prod2 (M,N))) = TopStruct (# the carrier of ( max-Prod2 (M,N)), ( Family_open_set ( max-Prod2 (M,N))) #) by PCOMPS_1:def 5;

      

       A2: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      

       A3: ( TopSpaceMetr N) = TopStruct (# the carrier of N, ( Family_open_set N) #) by PCOMPS_1:def 5;

      

       A4: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2

      .= the carrier of ( TopSpaceMetr ( max-Prod2 (M,N))) by A1, A2, A3, Def1;

      

       A5: the topology of [:S, T:] = { ( union A) where A be Subset-Family of [:S, T:] : A c= { [:X1, X2:] where X1 be Subset of S, X2 be Subset of T : X1 in the topology of S & X2 in the topology of T } } by BORSUK_1:def 2;

      the topology of [:S, T:] = the topology of ( TopSpaceMetr ( max-Prod2 (M,N)))

      proof

        thus the topology of [:S, T:] c= the topology of ( TopSpaceMetr ( max-Prod2 (M,N)))

        proof

          let X be object;

          assume

           A6: X in the topology of [:S, T:];

          then

          consider A be Subset-Family of [:S, T:] such that

           A7: X = ( union A) and

           A8: A c= { [:X1, X2:] where X1 be Subset of S, X2 be Subset of T : X1 in the topology of S & X2 in the topology of T } by A5;

          for x be Point of ( max-Prod2 (M,N)) st x in ( union A) holds ex r be Real st r > 0 & ( Ball (x,r)) c= ( union A)

          proof

            let x be Point of ( max-Prod2 (M,N));

            assume x in ( union A);

            then

            consider Z be set such that

             A9: x in Z and

             A10: Z in A by TARSKI:def 4;

            Z in { [:X1, X2:] where X1 be Subset of S, X2 be Subset of T : X1 in the topology of S & X2 in the topology of T } by A8, A10;

            then

            consider X1 be Subset of S, X2 be Subset of T such that

             A11: Z = [:X1, X2:] and

             A12: X1 in the topology of S and

             A13: X2 in the topology of T;

            consider z1,z2 be object such that

             A14: z1 in X1 and

             A15: z2 in X2 and

             A16: x = [z1, z2] by A9, A11, ZFMISC_1:def 2;

            reconsider z2 as Point of N by A3, A15;

            consider r2 be Real such that

             A17: r2 > 0 and

             A18: ( Ball (z2,r2)) c= X2 by A3, A13, A15, PCOMPS_1:def 4;

            reconsider z1 as Point of M by A2, A14;

            consider r1 be Real such that

             A19: r1 > 0 and

             A20: ( Ball (z1,r1)) c= X1 by A2, A12, A14, PCOMPS_1:def 4;

            take r = ( min (r1,r2));

            thus r > 0 by A19, A17, XXREAL_0: 15;

            let b be object;

            assume

             A21: b in ( Ball (x,r));

            then

            reconsider bb = b as Point of ( max-Prod2 (M,N));

            

             A22: ( dist (bb,x)) < r by A21, METRIC_1: 11;

            consider x1,y1 be Point of M, x2,y2 be Point of N such that

             A23: bb = [x1, x2] and

             A24: x = [y1, y2] and

             A25: (the distance of ( max-Prod2 (M,N)) . (bb,x)) = ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by Def1;

            z2 = y2 by A16, A24, XTUPLE_0: 1;

            then (the distance of N . (x2,z2)) <= ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by XXREAL_0: 25;

            then ( min (r1,r2)) <= r2 & (the distance of N . (x2,z2)) < r by A25, A22, XXREAL_0: 2, XXREAL_0: 17;

            then ( dist (x2,z2)) < r2 by XXREAL_0: 2;

            then

             A26: x2 in ( Ball (z2,r2)) by METRIC_1: 11;

            z1 = y1 by A16, A24, XTUPLE_0: 1;

            then (the distance of M . (x1,z1)) <= ( max ((the distance of M . (x1,y1)),(the distance of N . (x2,y2)))) by XXREAL_0: 25;

            then ( min (r1,r2)) <= r1 & (the distance of M . (x1,z1)) < r by A25, A22, XXREAL_0: 2, XXREAL_0: 17;

            then ( dist (x1,z1)) < r1 by XXREAL_0: 2;

            then x1 in ( Ball (z1,r1)) by METRIC_1: 11;

            then b in [:X1, X2:] by A20, A18, A23, A26, ZFMISC_1: 87;

            hence thesis by A10, A11, TARSKI:def 4;

          end;

          hence thesis by A1, A4, A6, PCOMPS_1:def 4, A7;

        end;

        let X be object;

        assume

         A27: X in the topology of ( TopSpaceMetr ( max-Prod2 (M,N)));

        then

        reconsider Y = X as Subset of [:S, T:] by A4;

        

         A28: ( Base-Appr Y) = { [:X1, Y1:] where X1 be Subset of S, Y1 be Subset of T : [:X1, Y1:] c= Y & X1 is open & Y1 is open } by BORSUK_1:def 3;

        

         A29: ( union ( Base-Appr Y)) = Y

        proof

          thus ( union ( Base-Appr Y)) c= Y by BORSUK_1: 12;

          let u be object;

          assume

           A30: u in Y;

          then

          reconsider uu = u as Point of ( max-Prod2 (M,N)) by A1, A4;

          consider r be Real such that

           A31: r > 0 and

           A32: ( Ball (uu,r)) c= Y by A1, A27, A30, PCOMPS_1:def 4;

          uu in the carrier of ( max-Prod2 (M,N));

          then uu in [:the carrier of M, the carrier of N:] by Def1;

          then

          consider u1,u2 be object such that

           A33: u1 in the carrier of M and

           A34: u2 in the carrier of N and

           A35: u = [u1, u2] by ZFMISC_1:def 2;

          reconsider u2 as Point of N by A34;

          reconsider u1 as Point of M by A33;

          reconsider B2 = ( Ball (u2,r)) as Subset of T by A3;

          reconsider B1 = ( Ball (u1,r)) as Subset of S by A2;

          u1 in ( Ball (u1,r)) & u2 in ( Ball (u2,r)) by A31, TBSP_1: 11;

          then

           A36: u in [:B1, B2:] by A35, ZFMISC_1: 87;

          

           A37: [:B1, B2:] c= Y

          proof

            let x be object;

            assume x in [:B1, B2:];

            then

            consider x1,x2 be object such that

             A38: x1 in B1 and

             A39: x2 in B2 and

             A40: x = [x1, x2] by ZFMISC_1:def 2;

            reconsider x2 as Point of N by A39;

            reconsider x1 as Point of M by A38;

            consider p1,p2 be Point of M, q1,q2 be Point of N such that

             A41: uu = [p1, q1] & [x1, x2] = [p2, q2] and

             A42: (the distance of ( max-Prod2 (M,N)) . (uu, [x1, x2])) = ( max ((the distance of M . (p1,p2)),(the distance of N . (q1,q2)))) by Def1;

            u2 = q1 & x2 = q2 by A35, A41, XTUPLE_0: 1;

            then

             A43: ( dist (q1,q2)) < r by A39, METRIC_1: 11;

            u1 = p1 & x1 = p2 by A35, A41, XTUPLE_0: 1;

            then ( dist (p1,p2)) < r by A38, METRIC_1: 11;

            then ( dist (uu, [x1, x2])) < r by A42, A43, XXREAL_0: 16;

            then x in ( Ball (uu,r)) by A40, METRIC_1: 11;

            hence thesis by A32;

          end;

          B1 is open & B2 is open by TOPMETR: 14;

          then [:B1, B2:] in ( Base-Appr Y) by A28, A37;

          hence thesis by A36, TARSKI:def 4;

        end;

        ( Base-Appr Y) c= { [:X1, Y1:] where X1 be Subset of S, Y1 be Subset of T : X1 in the topology of S & Y1 in the topology of T }

        proof

          let A be object;

          assume A in ( Base-Appr Y);

          then

          consider X1 be Subset of S, Y1 be Subset of T such that

           A44: A = [:X1, Y1:] and [:X1, Y1:] c= Y and

           A45: X1 is open & Y1 is open by A28;

          X1 in the topology of S & Y1 in the topology of T by A45;

          hence thesis by A44;

        end;

        hence thesis by A5, A29;

      end;

      hence thesis by A4;

    end;

    theorem :: TOPREAL7:24

    the carrier of M = the carrier of N & (for m be Point of M, n be Point of N, r be Real st r > 0 & m = n holds ex r1 be Real st r1 > 0 & ( Ball (n,r1)) c= ( Ball (m,r))) & (for m be Point of M, n be Point of N, r be Real st r > 0 & m = n holds ex r1 be Real st r1 > 0 & ( Ball (m,r1)) c= ( Ball (n,r))) implies ( TopSpaceMetr M) = ( TopSpaceMetr N)

    proof

      assume that

       A1: the carrier of M = the carrier of N and

       A2: for m be Point of M, n be Point of N, r be Real st r > 0 & m = n holds ex r1 be Real st r1 > 0 & ( Ball (n,r1)) c= ( Ball (m,r)) and

       A3: for m be Point of M, n be Point of N, r be Real st r > 0 & m = n holds ex r1 be Real st r1 > 0 & ( Ball (m,r1)) c= ( Ball (n,r));

      

       A4: ( Family_open_set M) = ( Family_open_set N)

      proof

        thus ( Family_open_set M) c= ( Family_open_set N)

        proof

          let X be object;

          reconsider XX = X as set by TARSKI: 1;

          assume

           A5: X in ( Family_open_set M);

          for n be Point of N st n in XX holds ex r be Real st r > 0 & ( Ball (n,r)) c= XX

          proof

            let n be Point of N such that

             A6: n in XX;

            reconsider m = n as Point of M by A1;

            consider r be Real such that

             A7: r > 0 and

             A8: ( Ball (m,r)) c= XX by A5, A6, PCOMPS_1:def 4;

            consider r1 be Real such that

             A9: r1 > 0 & ( Ball (n,r1)) c= ( Ball (m,r)) by A2, A7;

            take r1;

            thus thesis by A8, A9;

          end;

          hence thesis by A1, A5, PCOMPS_1:def 4;

        end;

        let X be object;

        reconsider XX = X as set by TARSKI: 1;

        assume

         A10: X in ( Family_open_set N);

        for m be Point of M st m in XX holds ex r be Real st r > 0 & ( Ball (m,r)) c= XX

        proof

          let m be Point of M such that

           A11: m in XX;

          reconsider n = m as Point of N by A1;

          consider r be Real such that

           A12: r > 0 and

           A13: ( Ball (n,r)) c= XX by A10, A11, PCOMPS_1:def 4;

          consider r1 be Real such that

           A14: r1 > 0 & ( Ball (m,r1)) c= ( Ball (n,r)) by A3, A12;

          take r1;

          thus thesis by A13, A14;

        end;

        hence thesis by A1, A10, PCOMPS_1:def 4;

      end;

      ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      hence thesis by A1, A4, PCOMPS_1:def 5;

    end;

    

     Lm2: ex f be Function of [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):], ( TopSpaceMetr ( Euclid (i + j))) st f is being_homeomorphism & for fi,fj be FinSequence st [fi, fj] in ( dom f) holds (f . (fi,fj)) = (fi ^ fj)

    proof

      set ci = the carrier of ( Euclid i), cj = the carrier of ( Euclid j), cij = the carrier of ( Euclid (i + j));

      defpred P[ Element of ci, Element of cj, set] means ex fi,fj be FinSequence of REAL st fi = $1 & fj = $2 & $3 = (fi ^ fj);

      

       A1: the carrier of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))) = the carrier of ( max-Prod2 (( Euclid i),( Euclid j))) by TOPMETR: 12;

      

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

      proof

        let x be Element of ci, y be Element of cj;

        x is Element of ( REAL i) & y is Element of ( REAL j);

        then

        reconsider fi = x, fj = y as FinSequence of REAL ;

        (fi ^ fj) is Tuple of (i + j), REAL by FINSEQ_2: 107;

        then

        reconsider u = (fi ^ fj) as Element of cij by FINSEQ_2: 131;

        take u;

        thus thesis;

      end;

      consider f be Function of [:ci, cj:], cij such that

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

      

       A4: [:ci, cj:] = the carrier of ( max-Prod2 (( Euclid i),( Euclid j))) by Def1;

      the carrier of ( TopSpaceMetr ( Euclid (i + j))) = cij by TOPMETR: 12;

      then

      reconsider f as Function of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))), ( TopSpaceMetr ( Euclid (i + j))) by A4, A1;

      

       A5: [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):] = ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))) by Th23;

      then

      reconsider f as Function of [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):], ( TopSpaceMetr ( Euclid (i + j)));

      take f;

      thus ( dom f) = ( [#] [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):]) by FUNCT_2:def 1;

      thus

       A6: ( rng f) = ( [#] ( TopSpaceMetr ( Euclid (i + j))))

      proof

        thus ( rng f) c= ( [#] ( TopSpaceMetr ( Euclid (i + j))));

        let y be object;

        assume y in ( [#] ( TopSpaceMetr ( Euclid (i + j))));

        then

        reconsider k = y as Element of ( REAL (i + j)) by TOPMETR: 12;

        ( len k) = (i + j) by CARD_1:def 7;

        then

        consider g,h be FinSequence of REAL such that

         A7: ( len g) = i & ( len h) = j and

         A8: k = (g ^ h) by FINSEQ_2: 23;

        

         A9: g in ci & h in cj by A7, Th16;

        then [g, h] in [:ci, cj:] by ZFMISC_1: 87;

        then

         A10: [g, h] in ( dom f) by FUNCT_2:def 1;

        ex fi,fj be FinSequence of REAL st fi = g & fj = h & (f . (g,h)) = (fi ^ fj) by A3, A9;

        hence thesis by A8, A10, FUNCT_1:def 3;

      end;

      thus

       A11: f is one-to-one

      proof

        let x1,x2 be object;

        assume x1 in ( dom f);

        then

        consider x1a,x1b be object such that

         A12: x1a in ci and

         A13: x1b in cj and

         A14: x1 = [x1a, x1b] by A4, A1, A5, ZFMISC_1:def 2;

        assume x2 in ( dom f);

        then

        consider x2a,x2b be object such that

         A15: x2a in ci and

         A16: x2b in cj and

         A17: x2 = [x2a, x2b] by A4, A1, A5, ZFMISC_1:def 2;

        assume

         A18: (f . x1) = (f . x2);

        consider fi1,fj1 be FinSequence of REAL such that

         A19: fi1 = x1a and

         A20: fj1 = x1b and

         A21: (f . (x1a,x1b)) = (fi1 ^ fj1) by A3, A12, A13;

        consider fi2,fj2 be FinSequence of REAL such that

         A22: fi2 = x2a and

         A23: fj2 = x2b and

         A24: (f . (x2a,x2b)) = (fi2 ^ fj2) by A3, A15, A16;

        ( len fj1) = j by A13, A20, CARD_1:def 7;

        then

         A25: ( len fj1) = ( len fj2) by A16, A23, CARD_1:def 7;

        

         A26: ( len fi1) = i by A12, A19, CARD_1:def 7;

        then ( len fi1) = ( len fi2) by A15, A22, CARD_1:def 7;

        then fi1 = fi2 by A14, A17, A21, A24, A25, A18, Th5;

        hence thesis by A14, A17, A19, A20, A21, A22, A23, A24, A26, A25, A18, Th5;

      end;

      

       A27: for P be Subset of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))) st P is open holds ((f " ) " P) is open

      proof

        let P be Subset of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j))));

        assume P is open;

        then P in the topology of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j))));

        then

         A28: P in ( Family_open_set ( max-Prod2 (( Euclid i),( Euclid j)))) by TOPMETR: 12;

        

         A29: for x be Point of ( Euclid (i + j)) st x in (f .: P) holds ex r be Real st r > 0 & ( Ball (x,r)) c= (f .: P)

        proof

          let x be Point of ( Euclid (i + j));

          assume x in (f .: P);

          then

          consider a be object such that

           A30: a in the carrier of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))) and

           A31: a in P and

           A32: x = (f . a) by FUNCT_2: 64;

          reconsider a as Point of ( max-Prod2 (( Euclid i),( Euclid j))) by A30, TOPMETR: 12;

          consider r be Real such that

           A33: r > 0 and

           A34: ( Ball (a,r)) c= P by A28, A31, PCOMPS_1:def 4;

          take r;

          thus r > 0 by A33;

          let b be object;

          assume

           A35: b in ( Ball (x,r));

          then

          reconsider bb = b as Point of ( Euclid (i + j));

          reconsider bb2 = bb, xx2 = x as Element of ( REAL (i + j));

          ( dist (bb,x)) < r by A35, METRIC_1: 11;

          then |.(bb2 - xx2).| < r by EUCLID:def 6;

          then

           A36: ( sqrt ( Sum ( sqr ( abs (bb2 - xx2))))) < r by EUCLID: 25;

          reconsider k = bb as Element of ( REAL (i + j));

          ( len k) = (i + j) by CARD_1:def 7;

          then

          consider g,h be FinSequence of REAL such that

           A37: ( len g) = i and

           A38: ( len h) = j and

           A39: k = (g ^ h) by FINSEQ_2: 23;

          reconsider hh = h as Point of ( Euclid j) by A38, Th16;

          reconsider gg = g as Point of ( Euclid i) by A37, Th16;

          consider g,h be FinSequence of REAL such that

           A40: g = gg and

           A41: h = hh and

           A42: (f . (gg,hh)) = (g ^ h) by A3;

          reconsider gg2 = gg, a12 = (a `1 ) as Element of ( REAL i);

          

           A43: ( max (( dist (gg,(a `1 ))),( dist (hh,(a `2 ))))) = ( dist (gg,(a `1 ))) or ( max (( dist (gg,(a `1 ))),( dist (hh,(a `2 ))))) = ( dist (hh,(a `2 ))) by XXREAL_0: 16;

          consider p,q be object such that

           A44: p in ci and

           A45: q in cj and

           A46: a = [p, q] by A4, ZFMISC_1:def 2;

          reconsider q as Element of cj by A45;

          reconsider p as Element of ci by A44;

          consider fi,fj be FinSequence of REAL such that

           A47: fi = p and

           A48: fj = q and

           A49: (f . (p,q)) = (fi ^ fj) by A3;

          

           A50: ( len fi) = i & ( len fj) = j by A47, A48, CARD_1:def 7;

          ( len g) = i & ( len h) = j by A40, A41, CARD_1:def 7;

          then ( sqrt ( Sum ( sqr (( abs (g - fi)) ^ ( abs (h - fj)))))) < r by A32, A39, A46, A49, A40, A41, A50, A36, Th15;

          then ( sqrt ( Sum (( sqr ( abs (g - fi))) ^ ( sqr ( abs (h - fj)))))) < r by Th10;

          then

           A51: ( sqrt (( Sum ( sqr ( abs (g - fi)))) + ( Sum ( sqr ( abs (h - fj)))))) < r by RVSUM_1: 75;

          reconsider hh2 = hh, a22 = (a `2 ) as Element of ( REAL j);

          

           A52: a22 = q by A46;

           0 <= ( Sum ( sqr ( abs (g - fi)))) by RVSUM_1: 86;

          then 0 <= ( Sum ( sqr ( abs (hh2 - a22)))) & (( Sum ( sqr ( abs (hh2 - a22)))) + 0 ) <= (( Sum ( sqr ( abs (g - fi)))) + ( Sum ( sqr ( abs (h - fj))))) by A48, A41, A52, RVSUM_1: 86, XREAL_1: 7;

          then ( sqrt ( Sum ( sqr ( abs (hh2 - a22))))) <= ( sqrt (( Sum ( sqr ( abs (g - fi)))) + ( Sum ( sqr ( abs (h - fj)))))) by SQUARE_1: 26;

          then ( sqrt ( Sum ( sqr ( abs (hh2 - a22))))) < r by A51, XXREAL_0: 2;

          then |.(hh2 - a22).| < r by EUCLID: 25;

          then

           A53: (( Pitag_dist j) . (hh2,a22)) < r by EUCLID:def 6;

          

           A54: a12 = p by A46;

           0 <= ( Sum ( sqr ( abs (h - fj)))) by RVSUM_1: 86;

          then 0 <= ( Sum ( sqr ( abs (gg2 - a12)))) & (( Sum ( sqr ( abs (gg2 - a12)))) + 0 ) <= (( Sum ( sqr ( abs (g - fi)))) + ( Sum ( sqr ( abs (h - fj))))) by A47, A40, A54, RVSUM_1: 86, XREAL_1: 7;

          then ( sqrt ( Sum ( sqr ( abs (gg2 - a12))))) <= ( sqrt (( Sum ( sqr ( abs (g - fi)))) + ( Sum ( sqr ( abs (h - fj)))))) by SQUARE_1: 26;

          then ( sqrt ( Sum ( sqr ( abs (gg2 - a12))))) < r by A51, XXREAL_0: 2;

          then |.(gg2 - a12).| < r by EUCLID: 25;

          then

           A55: (( Pitag_dist i) . (gg2,a12)) < r by EUCLID:def 6;

          ( dist ( [gg, hh], [(a `1 ), (a `2 )])) = ( max (( dist (gg,(a `1 ))),( dist (hh,(a `2 ))))) by Th18;

          then ( dist ( [gg, hh],a)) < r by A4, A55, A53, A43, MCART_1: 21;

          then [g, h] in ( Ball (a,r)) by A40, A41, METRIC_1: 11;

          then [g, h] in P by A34;

          hence thesis by A39, A40, A41, A42, FUNCT_2: 35;

        end;

        (f .: P) is Subset of ( Euclid (i + j)) by TOPMETR: 12;

        then (f .: P) in ( Family_open_set ( Euclid (i + j))) by A29, PCOMPS_1:def 4;

        then (f .: P) in the topology of ( TopSpaceMetr ( Euclid (i + j))) by TOPMETR: 12;

        hence ((f " ) " P) in the topology of ( TopSpaceMetr ( Euclid (i + j))) by A6, A11, A5, TOPS_2: 54;

      end;

      

       A56: for P be Subset of ( TopSpaceMetr ( Euclid (i + j))) st P is open holds (f " P) is open

      proof

        let P be Subset of ( TopSpaceMetr ( Euclid (i + j)));

        assume P is open;

        then P in the topology of ( TopSpaceMetr ( Euclid (i + j)));

        then

         A57: P in ( Family_open_set ( Euclid (i + j))) by TOPMETR: 12;

        

         A58: for x be Point of ( max-Prod2 (( Euclid i),( Euclid j))) st x in (f " P) holds ex r be Real st r > 0 & ( Ball (x,r)) c= (f " P)

        proof

          let x be Point of ( max-Prod2 (( Euclid i),( Euclid j)));

          assume

           A59: x in (f " P);

          then (f . x) in the carrier of ( TopSpaceMetr ( Euclid (i + j))) by FUNCT_2: 5;

          then

          reconsider fx = (f . x) as Point of ( Euclid (i + j)) by TOPMETR: 12;

          (f . x) in P by A59, FUNCT_2: 38;

          then

          consider r be Real such that

           A60: r > 0 and

           A61: ( Ball (fx,r)) c= P by A57, PCOMPS_1:def 4;

          take r1 = (r / 2);

          thus r1 > 0 by A60, XREAL_1: 139;

          let b be object;

          assume

           A62: b in ( Ball (x,r1));

          then

          reconsider bb = b as Point of ( max-Prod2 (( Euclid i),( Euclid j)));

          

           A63: ( dist (bb,x)) < r1 by A62, METRIC_1: 11;

          bb in the carrier of ( max-Prod2 (( Euclid i),( Euclid j)));

          then

           A64: bb in the carrier of ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j)))) by TOPMETR: 12;

          then (f . bb) in the carrier of ( TopSpaceMetr ( Euclid (i + j))) by FUNCT_2: 5;

          then

          reconsider fb = (f . b) as Point of ( Euclid (i + j)) by TOPMETR: 12;

          reconsider fbb = fb, fxx = fx as Element of ( REAL (i + j));

          consider b1,x1 be Point of ( Euclid i), b2,x2 be Point of ( Euclid j) such that

           A65: bb = [b1, b2] & x = [x1, x2] and (the distance of ( max-Prod2 (( Euclid i),( Euclid j))) . (bb,x)) = ( max ((the distance of ( Euclid i) . (b1,x1)),(the distance of ( Euclid j) . (b2,x2)))) by Def1;

          

           A66: ( dist ( [b1, b2], [x1, x2])) = ( max (( dist (b1,x1)),( dist (b2,x2)))) by Th18;

          ( dist (b2,x2)) <= ( max (( dist (b1,x1)),( dist (b2,x2)))) by XXREAL_0: 25;

          then

           A67: ( dist (b2,x2)) < r1 by A65, A66, A63, XXREAL_0: 2;

          reconsider x2i = x2, b2i = b2 as Element of ( REAL j);

          reconsider b1i = b1, x1i = x1 as Element of ( REAL i);

          consider b1f,b2f be FinSequence of REAL such that

           A68: b1f = b1 & b2f = b2 and

           A69: (f . (b1,b2)) = (b1f ^ b2f) by A3;

          

           A70: ( len b1f) = i & ( len b2f) = j by A68, CARD_1:def 7;

          ( dist (b1,x1)) <= ( max (( dist (b1,x1)),( dist (b2,x2)))) by XXREAL_0: 25;

          then ( dist (b1,x1)) < r1 by A65, A66, A63, XXREAL_0: 2;

          then

           A71: ((( Pitag_dist i) . (b1i,x1i)) + (( Pitag_dist j) . (b2i,x2i))) < (r1 + r1) by A67, XREAL_1: 8;

           0 <= ( Sum ( sqr (b1i - x1i))) & 0 <= ( Sum ( sqr (b2i - x2i))) by RVSUM_1: 86;

          then ( sqrt (( Sum ( sqr (b1i - x1i))) + ( Sum ( sqr (b2i - x2i))))) <= ( |.(b1i - x1i).| + ( sqrt ( Sum ( sqr (b2i - x2i))))) by SQUARE_1: 59;

          then ( sqrt (( Sum ( sqr (b1i - x1i))) + ( Sum ( sqr (b2i - x2i))))) <= ((( Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).|) by EUCLID:def 6;

          then

           A72: ( sqrt (( Sum ( sqr (b1i - x1i))) + ( Sum ( sqr (b2i - x2i))))) <= ((( Pitag_dist i) . (b1i,x1i)) + (( Pitag_dist j) . (b2i,x2i))) by EUCLID:def 6;

          consider x1f,x2f be FinSequence of REAL such that

           A73: x1f = x1 & x2f = x2 and

           A74: (f . (x1,x2)) = (x1f ^ x2f) by A3;

          

           A75: ( len x1f) = i & ( len x2f) = j by A73, CARD_1:def 7;

          (( Pitag_dist (i + j)) . (fbb,fxx)) = |.(fbb - fxx).| by EUCLID:def 6

          .= ( sqrt ( Sum ( sqr ( abs (fbb - fxx))))) by EUCLID: 25

          .= ( sqrt ( Sum ( sqr (( abs (b1i - x1i)) ^ ( abs (b2i - x2i)))))) by A65, A68, A69, A73, A74, A70, A75, Th15

          .= ( sqrt ( Sum (( sqr ( abs (b1i - x1i))) ^ ( sqr ( abs (b2i - x2i)))))) by Th10

          .= ( sqrt (( Sum ( sqr ( abs (b1i - x1i)))) + ( Sum ( sqr ( abs (b2i - x2i)))))) by RVSUM_1: 75

          .= ( sqrt (( Sum ( sqr ( abs (b1i - x1i)))) + ( Sum ( sqr (b2i - x2i))))) by EUCLID: 25

          .= ( sqrt (( Sum ( sqr (b1i - x1i))) + ( Sum ( sqr (b2i - x2i))))) by EUCLID: 25;

          then ( dist (fb,fx)) < r by A72, A71, XXREAL_0: 2;

          then (f . b) in ( Ball (fx,r)) by METRIC_1: 11;

          hence thesis by A61, A64, FUNCT_2: 38;

        end;

        (f " P) is Subset of ( max-Prod2 (( Euclid i),( Euclid j))) by A5, TOPMETR: 12;

        then (f " P) in ( Family_open_set ( max-Prod2 (( Euclid i),( Euclid j)))) by A58, PCOMPS_1:def 4;

        hence (f " P) in the topology of [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):] by A5, TOPMETR: 12;

      end;

      ( [#] ( TopSpaceMetr ( Euclid (i + j)))) <> {} ;

      hence f is continuous by A56, TOPS_2: 43;

      ( [#] ( TopSpaceMetr ( max-Prod2 (( Euclid i),( Euclid j))))) <> {} ;

      hence (f " ) is continuous by A27, A5, TOPS_2: 43;

      let fi,fj be FinSequence;

      assume

       A76: [fi, fj] in ( dom f);

      then

      reconsider Fi = fi as Element of ci by A1, A5, A4, ZFMISC_1: 87;

      reconsider Fj = fj as Element of cj by A76, A1, A5, A4, ZFMISC_1: 87;

       P[Fi, Fj, (f . (Fi,Fj))] by A3;

      hence (f . (fi,fj)) = (fi ^ fj);

    end;

    theorem :: TOPREAL7:25

    ( [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):],( TopSpaceMetr ( Euclid (i + j)))) are_homeomorphic

    proof

      consider f be Function of [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):], ( TopSpaceMetr ( Euclid (i + j))) such that

       A1: f is being_homeomorphism and for fi,fj be FinSequence st [fi, fj] in ( dom f) holds (f . (fi,fj)) = (fi ^ fj) by Lm2;

      take f;

      thus thesis by A1;

    end;

    theorem :: TOPREAL7:26

    ex f be Function of [:( TopSpaceMetr ( Euclid i)), ( TopSpaceMetr ( Euclid j)):], ( TopSpaceMetr ( Euclid (i + j))) st f is being_homeomorphism & for fi,fj be FinSequence st [fi, fj] in ( dom f) holds (f . (fi,fj)) = (fi ^ fj) by Lm2;