The Mizar article:

Homeomorphism between [:$\cal E^i_\rm T, \cal E^j_\rm T$:] and $\cal E^i+j_\rm T$

by
Artur Kornilowicz

Received February 21, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: TOPREAL7
[ MML identifier index ]


environ

 vocabulary FINSEQ_1, METRIC_1, SQUARE_1, RELAT_1, ARYTM_1, FUNCT_1, FINSEQ_2,
      RVSUM_1, ABSVALUE, EUCLID, PRE_TOPC, MCART_1, RELAT_2, PCOMPS_1, TARSKI,
      SETFAM_1, BORSUK_1, T_0TOPSP, SUBSET_1, ARYTM_3, COMPLEX1, RLVECT_1,
      ORDINAL2, TOPREAL7;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, MCART_1, DOMAIN_1, NUMBERS, XREAL_0, REAL_1, ABSVALUE, SQUARE_1,
      NAT_1, FINSEQ_1, RVSUM_1, FINSEQOP, STRUCT_0, PRE_TOPC, TOPS_2, PCOMPS_1,
      BORSUK_1, METRIC_1, EUCLID, FINSEQ_2, T_0TOPSP, GOBOARD1;
 constructors ABSVALUE, DOMAIN_1, FINSEQOP, GOBOARD1, INT_1, NAT_1, REAL_1,
      SEQ_1, SQUARE_1, T_0TOPSP, TOPS_2, BORSUK_1, MEMBERED;
 clusters SUBSET_1, INT_1, METRIC_1, PCOMPS_1, RELSET_1, STRUCT_0, EUCLID,
      MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FUNCT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2, T_0TOPSP,
      XBOOLE_0;
 theorems AXIOMS, BINOP_1, BORSUK_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3,
      FUNCT_1, FUNCT_2, INT_1, MCART_1, METRIC_1, NAT_1, PCOMPS_1, PRE_TOPC,
      REAL_1, REAL_2, RFUNCT_3, RLVECT_1, RVSUM_1, SQUARE_1, SPPOL_1, TARSKI,
      TBSP_1, TOPMETR, TOPREAL3, TOPREAL6, TOPS_2, ZFMISC_1, RELSET_1,
      XBOOLE_1, XCMPLX_1;
 schemes FUNCT_2;

begin

reserve i, j, n for Nat,
        f, g, h, k for FinSequence of REAL,
        M, N for non empty MetrSpace;

theorem Th1:
 for a, b being Real st max(a,b) <= a holds max(a,b) = a
  proof
    let a, b be Real;
    assume max(a,b) <= a;
    then max(a,b) < a or max(a,b) = a by REAL_1:def 5;
    hence thesis by SQUARE_1:46;
  end;

theorem Th2:
 for a, b, c, d being Real holds max(a+c,b+d) <= max(a,b) + max(c,d)
  proof
    let a, b, c, d be Real;
      a <= max(a,b) & c <= max(c,d) & b <= max(a,b) & d <=
 max(c,d) by SQUARE_1:46;
    then a+c <= max(a,b) + max(c,d) & b+d <= max(a,b) + max(c,d) by REAL_1:55;
    hence max(a+c,b+d) <= max(a,b) + max(c,d) by SQUARE_1:50;
  end;

theorem Th3:
 for a, b, c, d, e, f being 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 max(a,d) <= max(b+c,e+f) & max(b+c,e+f) <= max(b,e) + max(c,f)
     by Th2,RFUNCT_3:7;
    hence max(a,d) <= max(b,e) + max(c,f) by AXIOMS:22;
  end;

theorem
   for f, g being FinSequence holds dom g c= dom (f^g)
  proof
    let f, g be FinSequence;
      len g <= len f + len g by NAT_1:29;
    then Seg len g c= Seg (len f + len g) by FINSEQ_1:7;
    then dom g c= Seg (len f + len g) by FINSEQ_1:def 3;
    hence thesis by FINSEQ_1:def 7;
  end;

theorem Th5:
 for f, g being FinSequence st len f < i & i <= len f + len g holds
  i - len f in dom g
  proof
    let f, g be FinSequence such that
A1:   len f < i and
A2:   i <= len f + len g;
A3: i-len f is Nat by A1,INT_1:18;
      i-len f > len f-len f by A1,REAL_1:92;
    then i-len f > 0 by XCMPLX_1:14;
then A4: 1 <= i-len f by A3,RLVECT_1:99;
      i-len f <= len f + len g - len f by A2,REAL_1:49;
    then i-len f <= len f - len f + len g by XCMPLX_1:29;
    then i-len f <= 0 + len g by XCMPLX_1:14;
    hence i-len f in dom g by A3,A4,FINSEQ_3:27;
  end;

theorem Th6:
 for f, g, h, k being 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 st 1 <= i & i <= len f holds f.i = h.i
    proof
      let i;
      assume 1 <= i & i <= len f;
then A5:   i in dom f & i in dom h by A2,FINSEQ_3:27;
      hence f.i = (f^g).i by FINSEQ_1:def 7
         .= h.i by A1,A5,FINSEQ_1:def 7;
    end;
      for i st 1 <= i & i <= len g holds g.i = k.i
    proof
      let i;
      assume 1 <= i & i <= len g;
then A6:   i in dom g & i in dom k by A3,FINSEQ_3:27;
      hence g.i = (f^g).(len f +i) by FINSEQ_1:def 7
         .= k.i by A1,A2,A6,FINSEQ_1:def 7;
    end;
    hence f = h & g = k by A2,A3,A4,FINSEQ_1:18;
  end;

theorem 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:110;
    assume len f = len g or dom f = dom g;
    then len f = len g by FINSEQ_3:31;
    then reconsider g1 = g as Element of (len f)-tuples_on REAL by FINSEQ_2:110
;
      f1+g1 is Element of (len f)-tuples_on REAL;
    hence len (f+g) = len f by FINSEQ_2:109;
    hence thesis by FINSEQ_3:31;
  end;

theorem Th8:
 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:110;
    assume len f = len g or dom f = dom g;
    then len f = len g by FINSEQ_3:31;
    then reconsider g1 = g as Element of (len f)-tuples_on REAL by FINSEQ_2:110
;
      f1-g1 is Element of (len f)-tuples_on REAL;
    hence len (f-g) = len f by FINSEQ_2:109;
    hence thesis by FINSEQ_3:31;
  end;

theorem Th9:
 len f = len sqr f & dom f = dom sqr f
  proof
      rng f c= REAL & dom sqrreal = REAL by FINSEQ_1:def 4,FUNCT_2:def 1;
    hence len f = len (sqrreal*f) by FINSEQ_2:33
       .= len sqr f by RVSUM_1:def 8;
    hence thesis by FINSEQ_3:31;
  end;

theorem Th10:
 len f = len abs f & dom f = dom abs f
  proof
      rng f c= REAL & dom absreal = REAL by FINSEQ_1:def 4,FUNCT_2:def 1;
    hence len f = len (absreal*f) by FINSEQ_2:33
       .= len abs f by EUCLID:def 3;
    hence thesis by FINSEQ_3:31;
  end;

theorem Th11:
 sqr (f^g) = sqr f ^ sqr g
  proof
A1: len f = len sqr f by Th9;
A2: len g = len sqr g by Th9;
A3: len(f^g) = len f + len g by FINSEQ_1:35;
A4: len sqr (f^g) = len (f^g) by Th9;
then A5: len (sqr (f^g)) = len (sqr f ^ sqr g) by A1,A2,A3,FINSEQ_1:35;
      for i st 1 <= i & i <= len sqr (f^g) holds sqr (f^g).i = (sqr f ^ sqr g).
i
    proof
      let i;
      assume
A6:     1 <= i & i <= len sqr (f^g);
then A7:   i in dom (f^g) by A4,FINSEQ_3:27;
      per cases;
      suppose
A8:     i in dom f;
then A9:   i in dom sqr f by Th9;
      thus sqr (f^g).i = (sqrreal*(f^g)).i by RVSUM_1:def 8
        .= sqrreal.((f^g).i) by A7,FUNCT_1:23
        .= sqrreal.(f.i) by A8,FINSEQ_1:def 7
        .= (f.i)^2 by RVSUM_1:def 2
        .= (sqr f).i by RVSUM_1:78
        .= (sqr f ^ sqr g).i by A9,FINSEQ_1:def 7;
      suppose not i in dom f;
then A10:   len f < i & i <= len(f^g) by A6,Th9,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A11:   i <= len(sqr f ^ sqr g) by A1,A2,A3,A4,A6,FINSEQ_1:35;
      thus sqr (f^g).i = (sqrreal*(f^g)).i by RVSUM_1:def 8
        .= sqrreal.((f^g).i) by A7,FUNCT_1:23
        .= sqrreal.(g.j) by A10,FINSEQ_1:37
        .= (g.j)^2 by RVSUM_1:def 2
        .= (sqr g).j by RVSUM_1:78
        .= (sqr f ^ sqr g).i by A1,A10,A11,FINSEQ_1:37;
    end;
    hence sqr (f^g) = sqr f ^ sqr g by A5,FINSEQ_1:18;
  end;

theorem
   abs (f^g) = abs f ^ abs g
  proof
A1: len f = len abs f by Th10;
A2: len g = len abs g by Th10;
A3: len(f^g) = len f + len g by FINSEQ_1:35;
A4: len abs (f^g) = len (f^g) by Th10;
then A5: len (abs (f^g)) = len (abs f ^ abs g) by A1,A2,A3,FINSEQ_1:35;
      for i st 1 <= i & i <=
 len abs (f^g) holds (abs (f^g)).i = (abs f ^ abs g).i
    proof
      let i;
      assume
A6:     1 <= i & i <= len abs (f^g);
then A7:   i in dom (f^g) by A4,FINSEQ_3:27;
      per cases;
      suppose
A8:     i in dom f;
then A9:   i in dom abs f by Th10;
      thus (abs (f^g)).i = (absreal*(f^g)).i by EUCLID:def 3
        .= absreal.((f^g).i) by A7,FUNCT_1:23
        .= absreal.(f.i) by A8,FINSEQ_1:def 7
        .= abs(f.i) by EUCLID:def 2
        .= (abs f).i by A9,TOPREAL6:17
        .= (abs f ^ abs g).i by A9,FINSEQ_1:def 7;
      suppose not i in dom f;
then A10:   len f < i & i <= len(f^g) by A6,Th10,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A11:   j in dom abs g by A2,A3,A10,Th5;
A12:   i <= len(abs f ^ abs g) by A1,A2,A3,A4,A6,FINSEQ_1:35;
      thus (abs (f^g)).i = (absreal*(f^g)).i by EUCLID:def 3
        .= absreal.((f^g).i) by A7,FUNCT_1:23
        .= absreal.(g.j) by A10,FINSEQ_1:37
        .= abs(g.j) by EUCLID:def 2
        .= (abs g).j by A11,TOPREAL6:17
        .= (abs f ^ abs g).i by A1,A10,A12,FINSEQ_1:37;
    end;
    hence abs (f^g) = abs f ^ abs g by A5,FINSEQ_1:18;
  end;

theorem
   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:35;
A4: len (h^k) = len h + len k by FINSEQ_1:35;
A5: len sqr (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 sqr (f+h) + len (g+k) by Th9
     .= len sqr (f+h) + len sqr (g+k) by Th9
     .= len (sqr (f+h) ^ sqr (g+k)) by FINSEQ_1:35;
      for i 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;
      assume
A6:     1 <= i & i <= len sqr (f^g + h^k);
   then i in dom sqr (f^g + h^k) by FINSEQ_3:27;
then A7:   i in dom (f^g + h^k) by Th9;
      per cases;
      suppose
A8:     i in dom f;
then A9:   i in dom h by A1,FINSEQ_3:31;
A10:   i in dom (f+h) by A1,A8,Th7;
then A11:   i in dom sqr (f+h) by Th9;
      thus (sqr (f^g + h^k)).i = ((f^g + h^k).i)^2 by RVSUM_1:78
        .= ((f^g).i + (h^k).i)^2 by A7,RVSUM_1:26
        .= (f.i + (h^k).i)^2 by A8,FINSEQ_1:def 7
        .= (f.i + h.i)^2 by A9,FINSEQ_1:def 7
        .= ((f+h).i)^2 by A10,RVSUM_1:26
        .= (sqr (f+h)).i by RVSUM_1:78
        .= (sqr (f+h) ^ sqr (g+k)).i by A11,FINSEQ_1:def 7;
      suppose
A12:     not i in dom f;
        i <= len (f^g + h^k) by A6,Th9;
then A13:   len f < i & i <= len (f^g) by A1,A2,A3,A4,A6,A12,Th7,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A14:   len (f+h) < i by A1,A13,Th7;
        i <= len (f+h) + len g by A1,A3,A13,Th7;
      then i <= len (f+h) + len (g+k) by A2,Th7;
      then i - len (f+h) in dom (g+k) by A14,Th5;
then A15:   j in dom (g+k) by A1,Th7;
A16:   len sqr (f+h) < i by A14,Th9;
        len f = len (f+h) by A1,Th7;
then A17:   j = i - len sqr (f+h) by Th9;
      thus (sqr (f^g + h^k)).i = ((f^g + h^k).i)^2 by RVSUM_1:78
        .= ((f^g).i + (h^k).i)^2 by A7,RVSUM_1:26
        .= (g.j + (h^k).i)^2 by A13,FINSEQ_1:37
        .= (g.j + k.j)^2 by A1,A2,A3,A4,A13,FINSEQ_1:37
        .= ((g+k).j)^2 by A15,RVSUM_1:26
        .= (sqr (g+k)).j by RVSUM_1:78
        .= (sqr (f+h) ^ sqr (g+k)).i by A5,A6,A16,A17,FINSEQ_1:37;
    end;
    hence sqr (f^g + h^k) = sqr (f+h) ^ sqr (g+k) by A5,FINSEQ_1:18;
  end;

theorem
   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:35;
A4: len (h^k) = len h + len k by FINSEQ_1:35;
A5: len abs (f^g + h^k) = len (f^g + h^k) by Th10
     .= 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 Th10
     .= len abs (f+h) + len abs (g+k) by Th10
     .= len (abs (f+h) ^ abs (g+k)) by FINSEQ_1:35;
      for i 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;
      assume
A6:     1 <= i & i <= len abs (f^g + h^k);
then A7:   i in dom abs (f^g + h^k) by FINSEQ_3:27;
then A8:   i in dom (f^g + h^k) by Th10;
      per cases;
      suppose
A9:     i in dom f;
then A10:   i in dom h by A1,FINSEQ_3:31;
A11:   i in dom (f+h) by A1,A9,Th7;
then A12:   i in dom abs (f+h) by Th10;
      thus (abs (f^g + h^k)).i = abs( (f^g + h^k).i ) by A7,TOPREAL6:17
        .= abs( (f^g).i + (h^k).i ) by A8,RVSUM_1:26
        .= abs( f.i + (h^k).i ) by A9,FINSEQ_1:def 7
        .= abs( f.i + h.i ) by A10,FINSEQ_1:def 7
        .= abs( (f+h).i ) by A11,RVSUM_1:26
        .= (abs (f+h)).i by A12,TOPREAL6:17
        .= (abs (f+h) ^ abs (g+k)).i by A12,FINSEQ_1:def 7;
      suppose
A13:     not i in dom f;
        i <= len (f^g + h^k) by A6,Th10;
then A14:   len f < i & i <= len (f^g) by A1,A2,A3,A4,A6,A13,Th7,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A15:   len (f+h) < i by A1,A14,Th7;
        i <= len (f+h) + len g by A1,A3,A14,Th7;
      then i <= len (f+h) + len (g+k) by A2,Th7;
      then i - len (f+h) in dom (g+k) by A15,Th5;
then A16:   j in dom (g+k) by A1,Th7;
then A17:   j in dom abs (g+k) by Th10;
A18:   len abs (f+h) < i by A15,Th10;
        len f = len (f+h) by A1,Th7;
then A19:   j = i - len abs (f+h) by Th10;
      thus (abs (f^g + h^k)).i = abs( (f^g + h^k).i ) by A7,TOPREAL6:17
        .= abs( (f^g).i + (h^k).i ) by A8,RVSUM_1:26
        .= abs( g.j + (h^k).i ) by A14,FINSEQ_1:37
        .= abs( g.j + k.j ) by A1,A2,A3,A4,A14,FINSEQ_1:37
        .= abs( (g+k).j ) by A16,RVSUM_1:26
        .= (abs (g+k)).j by A17,TOPREAL6:17
        .= (abs (f+h) ^ abs (g+k)).i by A5,A6,A18,A19,FINSEQ_1:37;
    end;
    hence abs (f^g + h^k) = abs (f+h) ^ abs (g+k) by A5,FINSEQ_1:18;
  end;

theorem
   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:35;
A4: len (h^k) = len h + len k by FINSEQ_1:35;
A5: len sqr (f^g - h^k) = len (f^g - h^k) by Th9
     .= len (f^g) by A1,A2,A3,A4,Th8
     .= len (f-h) + len g by A1,A3,Th8
     .= len (f-h) + len (g-k) by A2,Th8
     .= len sqr (f-h) + len (g-k) by Th9
     .= len sqr (f-h) + len sqr (g-k) by Th9
     .= len (sqr (f-h) ^ sqr (g-k)) by FINSEQ_1:35;
      for i 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;
      assume
A6:     1 <= i & i <= len sqr (f^g - h^k);
   then i in dom sqr (f^g - h^k) by FINSEQ_3:27;
then A7:   i in dom (f^g - h^k) by Th9;
      per cases;
      suppose
A8:     i in dom f;
then A9:   i in dom h by A1,FINSEQ_3:31;
A10:   i in dom (f-h) by A1,A8,Th8;
then A11:   i in dom sqr (f-h) by Th9;
      thus (sqr (f^g - h^k)).i = ((f^g - h^k).i)^2 by RVSUM_1:78
        .= ((f^g).i - (h^k).i)^2 by A7,RVSUM_1:47
        .= (f.i - (h^k).i)^2 by A8,FINSEQ_1:def 7
        .= (f.i - h.i)^2 by A9,FINSEQ_1:def 7
        .= ((f-h).i)^2 by A10,RVSUM_1:47
        .= (sqr (f-h)).i by RVSUM_1:78
        .= (sqr (f-h) ^ sqr (g-k)).i by A11,FINSEQ_1:def 7;
      suppose
A12:     not i in dom f;
        i <= len (f^g - h^k) by A6,Th9;
then A13:   len f < i & i <= len (f^g) by A1,A2,A3,A4,A6,A12,Th8,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A14:   len (f-h) < i by A1,A13,Th8;
        i <= len (f-h) + len g by A1,A3,A13,Th8;
      then i <= len (f-h) + len (g-k) by A2,Th8;
      then i - len (f-h) in dom (g-k) by A14,Th5;
then A15:   j in dom (g-k) by A1,Th8;
A16:   len sqr (f-h) < i by A14,Th9;
        len f = len (f-h) by A1,Th8;
then A17:   j = i - len sqr (f-h) by Th9;
      thus (sqr (f^g - h^k)).i = ((f^g - h^k).i)^2 by RVSUM_1:78
        .= ((f^g).i - (h^k).i)^2 by A7,RVSUM_1:47
        .= (g.j - (h^k).i)^2 by A13,FINSEQ_1:37
        .= (g.j - k.j)^2 by A1,A2,A3,A4,A13,FINSEQ_1:37
        .= ((g-k).j)^2 by A15,RVSUM_1:47
        .= (sqr (g-k)).j by RVSUM_1:78
        .= (sqr (f-h) ^ sqr (g-k)).i by A5,A6,A16,A17,FINSEQ_1:37;
    end;
    hence sqr (f^g - h^k) = sqr (f-h) ^ sqr (g-k) by A5,FINSEQ_1:18;
  end;

theorem Th16:
 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:35;
A4: len (h^k) = len h + len k by FINSEQ_1:35;
A5: len abs (f^g - h^k) = len (f^g - h^k) by Th10
     .= len (f^g) by A1,A2,A3,A4,Th8
     .= len (f-h) + len g by A1,A3,Th8
     .= len (f-h) + len (g-k) by A2,Th8
     .= len abs (f-h) + len (g-k) by Th10
     .= len abs (f-h) + len abs (g-k) by Th10
     .= len (abs (f-h) ^ abs (g-k)) by FINSEQ_1:35;
      for i 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;
      assume
A6:     1 <= i & i <= len abs (f^g - h^k);
then A7:   i in dom abs (f^g - h^k) by FINSEQ_3:27;
then A8:   i in dom (f^g - h^k) by Th10;
      per cases;
      suppose
A9:     i in dom f;
then A10:   i in dom h by A1,FINSEQ_3:31;
A11:   i in dom (f-h) by A1,A9,Th8;
then A12:   i in dom abs (f-h) by Th10;
      thus (abs (f^g - h^k)).i = abs( (f^g - h^k).i ) by A7,TOPREAL6:17
        .= abs( (f^g).i - (h^k).i ) by A8,RVSUM_1:47
        .= abs( f.i - (h^k).i ) by A9,FINSEQ_1:def 7
        .= abs( f.i - h.i ) by A10,FINSEQ_1:def 7
        .= abs( (f-h).i ) by A11,RVSUM_1:47
        .= (abs (f-h)).i by A12,TOPREAL6:17
        .= (abs (f-h) ^ abs (g-k)).i by A12,FINSEQ_1:def 7;
      suppose
A13:     not i in dom f;
        i <= len (f^g - h^k) by A6,Th10;
then A14:   len f < i & i <= len (f^g) by A1,A2,A3,A4,A6,A13,Th8,FINSEQ_3:27;
      then reconsider j = i - len f as Nat by INT_1:18;
A15:   len (f-h) < i by A1,A14,Th8;
        i <= len (f-h) + len g by A1,A3,A14,Th8;
      then i <= len (f-h) + len (g-k) by A2,Th8;
      then i - len (f-h) in dom (g-k) by A15,Th5;
then A16:   j in dom (g-k) by A1,Th8;
then A17:   j in dom abs (g-k) by Th10;
A18:   len abs (f-h) < i by A15,Th10;
        len f = len (f-h) by A1,Th8;
then A19:   j = i - len abs (f-h) by Th10;
      thus (abs (f^g - h^k)).i = abs( (f^g - h^k).i ) by A7,TOPREAL6:17
        .= abs( (f^g).i - (h^k).i ) by A8,RVSUM_1:47
        .= abs( g.j - (h^k).i ) by A14,FINSEQ_1:37
        .= abs( g.j - k.j ) by A1,A2,A3,A4,A14,FINSEQ_1:37
        .= abs( (g-k).j ) by A16,RVSUM_1:47
        .= (abs (g-k)).j by A17,TOPREAL6:17
        .= (abs (f-h) ^ abs (g-k)).i by A5,A6,A18,A19,FINSEQ_1:37;
    end;
    hence thesis by A5,FINSEQ_1:18;
  end;

theorem Th17:
 len f = n implies f in the carrier of Euclid n
  proof
    assume
A1:   len f = n;
A2: f in REAL* by FINSEQ_1:def 11;
      n-tuples_on REAL = { s where s is Element of REAL*: len s = n }
      by FINSEQ_2:def 4;
    then f in n-tuples_on REAL by A1,A2;
    then f in REAL n by EUCLID:def 1;
    then f is Point of Euclid n by SPPOL_1:19;
    hence thesis;
  end;

theorem
   len f = n implies f in the carrier of TOP-REAL n
  proof
    assume len f = n;
    then f in the carrier of Euclid n by Th17;
    hence thesis by TOPREAL3:13;
  end;

theorem Th19:
 for f being FinSequence st f in the carrier of Euclid n holds len f = n
  proof
    let f be FinSequence;
    assume
A1:   f in the carrier of Euclid n;
      Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
    then f is Element of n-tuples_on REAL by A1,EUCLID:def 1;
    hence len f = n by FINSEQ_2:109;
  end;

definition let M, N be non empty MetrStruct;
 func max-Prod2(M,N) -> strict MetrStruct means :Def1:
  the carrier of it = [:the carrier of M,the carrier of N:] &
  for x, y being Point of it
   ex x1, y1 being Point of M,
      x2, y2 being 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
    set C = [:the carrier of M,the carrier of N:];
defpred P[set,set,set] means
 ex x1, y1 being Point of M,
    x2, y2 being Point of N st $1 = [x1,x2] & $2 = [y1,y2] &
  $3 = max ((the distance of M).(x1,y1),(the distance of N).(x2,y2));
A1: for x, y being Element of C ex u being 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;
      take max ((the distance of M).(x1,y1),(the distance of N).(x2,y2));
      take x1, y1, x2, y2;
      thus thesis by MCART_1:23;
    end;
    consider f being Function of [:C,C:], REAL such that
A2:   for x, y being Element of C holds P[x,y,f. [x,y]] from FuncEx2D(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 being Point of M,
             x2, y2 being 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,BINOP_1:def 1;
  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 being Point of A
      ex x1, y1 being Point of M,
         x2, y2 being 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 being Point of B
      ex x1, y1 being Point of M,
         x2, y2 being 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 being 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 being Point of M,
               x2, y2 being Point of N such that
A9:    a = [x1,x2] & b = [y1,y2] and
A10:    f.(a,b) = max ((the distance of M).(x1,y1),(the distance of N).(x2,y2))
         by A5;
      consider m1, n1 being Point of M,
               m2, n2 being Point of N such that
A11:    a = [m1,m2] & b = [n1,n2] and
A12:    g.(a,b) = max ((the distance of M).(m1,n1),(the distance of N).(m2,n2))
         by A4,A6,A7,A8;
A13:   x1 = m1 & x2 = m2 & y1 = n1 & y2 = n2 by A9,A11,ZFMISC_1:33;
      thus f. [a,b]
        = max ((the distance of M).(x1,y1),(the distance of N).(x2,y2))
          by A10,BINOP_1:def 1
       .= g. [a,b] by A12,A13,BINOP_1:def 1;
    end;
    hence thesis by A4,A6,FUNCT_2:118;
  end;
end;

definition 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;
 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);
 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;
    then x`1 in the carrier of M by MCART_1:10;
    hence thesis;
  end;
 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;
    then x`2 in the carrier of N by MCART_1:10;
    hence thesis;
  end;
end;

theorem Th20:
 for M, N being non empty MetrStruct,
     m1, m2 being Point of M, n1, n2 being 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 being Point of M,
             x2, y2 being Point of N such that
A1:   [m1,n1] = [x1,x2] & [m2,n2] = [y1,y2] and
A2:   (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;
A3: m1 = x1 & n1 = x2 & m2 = y1 & n2 = y2 by A1,ZFMISC_1:33;
      (the distance of max-Prod2(M,N)).([m1,n1],[m2,n2]) = dist([m1,n1],[m2,n2]
)
&
     (the distance of M).(m1,m2) = dist(m1,m2) &
      (the distance of N).(n1,n2) = dist(n1,n2) by METRIC_1:def 1;
    hence dist([m1,n1],[m2,n2]) = max (dist(m1,m2),dist(n1,n2)) by A2,A3;
  end;

theorem
   for M, N being non empty MetrStruct,
     m, n being 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 being Point of M,
             x2, y2 being Point of N such that
A1:   m = [x1,x2] & n = [y1,y2] and
A2:   (the distance of max-Prod2(M,N)).(m,n) =
       max ((the distance of M).(x1,y1),(the distance of N).(x2,y2)) by Def1;
A3: m`1 = x1 & n`1 = y1 & m`2 = x2 & n`2 = y2 by A1,MCART_1:7;
      (the distance of max-Prod2(M,N)).(m,n) = dist(m,n) &
     (the distance of M).(m`1,n`1) = dist(m`1,n`1) &
      (the distance of N).(m`2,n`2) = dist(m`2,n`2) by METRIC_1:def 1;
    hence dist(m,n) = max (dist(m`1,n`1),dist(m`2,n`2)) by A2,A3;
  end;

theorem Th22:
 for M, N being 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 being Point of M,
             x2, y2 being 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;
A3: x1 = y1 & x2 = y2 by A1,ZFMISC_1:33;
      the distance of M is Reflexive & the distance of N is Reflexive
      by METRIC_1:def 7;
    then (the distance of M).(x1,x1) = 0 & (the distance of N).(x2,x2) = 0
      by METRIC_1:def 3;
    hence (the distance of max-Prod2(M,N)).(a,a) = 0 by A2,A3;
  end;

definition let M, N be Reflexive (non empty MetrStruct);
 cluster max-Prod2(M,N) -> Reflexive;
coherence by Th22;
end;

Lm1:
 for M, N being 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;
    consider x1, y1 being Point of M,
             x2, y2 being Point of N such that
A2:   a = [x1,x2] & 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;
      0 <= dist(x1,y1) & 0 <= dist(x2,y2) by METRIC_1:5;
    then 0 <= (the distance of M).(x1,y1) & 0 <= (the distance of N).(x2,y2)
     by METRIC_1:def 1;
then A4: (the distance of M).(x1,y1) = 0 & (the distance of N).(x2,y2) = 0
      by A1,A3,Th1;
      the distance of M is discerning & the distance of N is discerning
      by METRIC_1:def 8;
    then x1 = y1 & x2 = y2 by A4,METRIC_1:def 4;
    hence a = b by A2;
  end;

theorem Th23:
 for M, N being 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 being Point of M,
             x2, y2 being Point of N such that
A1:   a = [x1,x2] & b = [y1,y2] and
A2:   (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 being Point of M,
             m2, n2 being Point of N such that
A3:   b = [m1,m2] & a = [n1,n2] and
A4:   (the distance of max-Prod2(M,N)).(b,a) =
       max ((the distance of M).(m1,n1),(the distance of N).(m2,n2)) by Def1;
      the distance of M is symmetric & the distance of N is symmetric
      by METRIC_1:def 9;
then A5: (the distance of M).(x1,y1) = (the distance of M).(y1,x1) &
      (the distance of N).(x2,y2) = (the distance of N).(y2,x2)
      by METRIC_1:def 5;
      y1 = m1 & y2 = m2 & x1 = n1 & x2 = n2 by A1,A3,ZFMISC_1:33;
    hence (the distance of max-Prod2(M,N)).(a,b) =
     (the distance of max-Prod2(M,N)).(b,a) by A2,A4,A5;
  end;

definition let M, N be symmetric (non empty MetrStruct);
 cluster max-Prod2(M,N) -> symmetric;
coherence by Th23;
end;

theorem Th24:
 for M, N being 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 being Point of M,
             x2, y2 being Point of N such that
A1:   a = [x1,x2] & b = [y1,y2] and
A2:   (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 being Point of M,
             m2, n2 being Point of N such that
A3:   b = [m1,m2] & c = [n1,n2] and
A4:   (the distance of max-Prod2(M,N)).(b,c) =
       max ((the distance of M).(m1,n1),(the distance of N).(m2,n2)) by Def1;
    consider p1, q1 being Point of M,
             p2, q2 being Point of N such that
A5:   a = [p1,p2] & c = [q1,q2] and
A6:   (the distance of max-Prod2(M,N)).(a,c) =
       max ((the distance of M).(p1,q1),(the distance of N).(p2,q2)) by Def1;
      the distance of M is triangle & the distance of N is triangle
      by METRIC_1:def 10;
then A7: (the distance of M).(p1,q1) <= (the distance of M).(p1,y1)
      + (the distance of M).(y1,q1) &
    (the distance of N).(p2,q2) <= (the distance of N).(p2,y2)
      + (the distance of N).(y2,q2) by METRIC_1:def 6;
      x1 = p1 & x2 = p2 & y1 = m1 & y2 = m2 & q1 = n1 & q2 = n2
     by A1,A3,A5,ZFMISC_1:33;
    hence (the distance of max-Prod2(M,N)).(a,c) <=
     (the distance of max-Prod2(M,N)).(a,b)
      + (the distance of max-Prod2(M,N)).(b,c)
     by A2,A4,A6,A7,Th3;
  end;

definition let M, N be triangle (non empty MetrStruct);
 cluster max-Prod2(M,N) -> triangle;
coherence by Th24;
end;

definition let M, N be non empty MetrSpace;
 cluster max-Prod2(M,N) -> discerning;
coherence by Lm1;
end;

theorem Th25:
 [:TopSpaceMetr M,TopSpaceMetr N:] = TopSpaceMetr max-Prod2(M,N)
  proof
    set S = TopSpaceMetr M,
        T = TopSpaceMetr N;
A1: the topology of [:S,T:] =
     { union A where A is Subset-Family of [:S,T:]:
      A c= { [:X1,X2:] where X1 is Subset of S,
                             X2 is Subset of T :
               X1 in the topology of S & X2 in the topology of T}}
      by BORSUK_1:def 5;
A2: TopSpaceMetr max-Prod2(M,N) =
     TopStruct (#the carrier of max-Prod2(M,N), Family_open_set max-Prod2(M,N)
#)
      by PCOMPS_1:def 6;
A3: TopSpaceMetr M =
     TopStruct (#the carrier of M, Family_open_set M#) by PCOMPS_1:def 6;
A4: TopSpaceMetr N =
     TopStruct (#the carrier of N, Family_open_set N#) by PCOMPS_1:def 6;
A5: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
       by BORSUK_1:def 5
     .= the carrier of TopSpaceMetr max-Prod2(M,N) by A2,A3,A4,Def1;
      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 set;
        assume
A6:       X in the topology of [:S,T:];
        then consider A being Subset-Family of [:S,T:] such that
A7:       X = union A and
A8:       A c= { [:X1,X2:] where X1 is Subset of S,
                                 X2 is Subset of T :
            X1 in the topology of S & X2 in the topology of T} by A1;
          for x being Point of max-Prod2(M,N) st x in X
         ex r being Real st r > 0 & Ball(x,r) c= X
        proof
          let x be Point of max-Prod2(M,N);
          assume x in X;
          then consider Z being set such that
A9:         x in Z and
A10:         Z in A by A7,TARSKI:def 4;
            Z in { [:X1,X2:] where X1 is Subset of S,
                                X2 is Subset of T :
             X1 in the topology of S & X2 in the topology of T} by A8,A10;
          then consider X1 being Subset of S,
                   X2 being 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 being set such that
A14:         z1 in X1 and
A15:         z2 in X2 and
A16:         x = [z1,z2] by A9,A11,ZFMISC_1:def 2;
          reconsider z1 as Point of M by A3,A14;
          reconsider z2 as Point of N by A4,A15;
          consider r1 being Real such that
A17:         r1 > 0 and
A18:         Ball(z1,r1) c= X1 by A3,A12,A14,PCOMPS_1:def 5;
          consider r2 being Real such that
A19:         r2 > 0 and
A20:         Ball(z2,r2) c= X2 by A4,A13,A15,PCOMPS_1:def 5;
          take r = min(r1,r2);
          thus r > 0 by A17,A19,SQUARE_1:38;
          let b be set;
          assume
A21:         b in Ball(x,r);
          then reconsider bb = b as Point of max-Prod2(M,N);
          consider x1, y1 being Point of M,
                   x2, y2 being Point of N such that
A22:         bb = [x1,x2] and
A23:         x = [y1,y2] and
A24:         (the distance of max-Prod2(M,N)).(bb,x) =
              max ((the distance of M).(x1,y1),(the distance of N).(x2,y2))
                by Def1;
A25:       z1 = y1 & z2 = y2 by A16,A23,ZFMISC_1:33;
            dist(bb,x) < r by A21,METRIC_1:12;
then A26:       (the distance of max-Prod2(M,N)).(bb,x) < r by METRIC_1:def 1;
A27:       min(r1,r2) <= r1 & min(r1,r2) <= r2 by SQUARE_1:35;
            (the distance of M).(x1,z1) <=
            max ((the distance of M).(x1,y1),(the distance of N).(x2,y2))
             by A25,SQUARE_1:46;
          then (the distance of M).(x1,z1) < r by A24,A26,AXIOMS:22;
          then (the distance of M).(x1,z1) < r1 by A27,AXIOMS:22;
          then dist(x1,z1) < r1 by METRIC_1:def 1;
then A28:       x1 in Ball(z1,r1) by METRIC_1:12;
            (the distance of N).(x2,z2) <=
            max ((the distance of M).(x1,y1),(the distance of N).(x2,y2))
             by A25,SQUARE_1:46;
          then (the distance of N).(x2,z2) < r by A24,A26,AXIOMS:22;
          then (the distance of N).(x2,z2) < r2 by A27,AXIOMS:22;
          then dist(x2,z2) < r2 by METRIC_1:def 1;
          then x2 in Ball(z2,r2) by METRIC_1:12;
          then b in [:X1,X2:] by A18,A20,A22,A28,ZFMISC_1:106;
          hence b in X by A7,A10,A11,TARSKI:def 4;
        end;
        hence X in the topology of TopSpaceMetr max-Prod2(M,N)
          by A2,A5,A6,PCOMPS_1:def 5;
      end;
      let X be set;
      assume
A29:     X in the topology of TopSpaceMetr max-Prod2(M,N);
      then reconsider Y = X as Subset of [:S,T:] by A5;
A30:   Base-Appr Y = { [:X1,Y1:] where X1 is Subset of S, Y1 is Subset of T :
        [:X1,Y1:] c= Y & X1 is open & Y1 is open} by BORSUK_1:def 6;
A31:   union Base-Appr Y = Y
      proof
        thus union Base-Appr Y c= Y by BORSUK_1:53;
        let u be set;
        assume
A32:       u in Y;
        then reconsider uu = u as Point of max-Prod2(M,N) by A2,A5;
        consider r being Real such that
A33:       r > 0 and
A34:       Ball(uu,r) c= Y by A2,A29,A32,PCOMPS_1:def 5;
          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 being set such that
A35:       u1 in the carrier of M and
A36:       u2 in the carrier of N and
A37:       u = [u1,u2] by ZFMISC_1:def 2;
        reconsider u1 as Point of M by A35;
        reconsider u2 as Point of N by A36;
        reconsider B1 = Ball(u1,r) as Subset of S by A3;
        reconsider B2 = Ball(u2,r) as Subset of T by A4;
          u1 in Ball(u1,r) & u2 in Ball(u2,r) by A33,TBSP_1:16;
then A38:     u in [:B1,B2:] by A37,ZFMISC_1:106;
A39:     [:B1,B2:] c= Y
        proof
          let x be set;
          assume x in [:B1,B2:];
          then consider x1, x2 being set such that
A40:         x1 in B1 and
A41:         x2 in B2 and
A42:         x = [x1,x2] by ZFMISC_1:def 2;
          reconsider x1 as Point of M by A40;
          reconsider x2 as Point of N by A41;
          consider p1, p2 being Point of M,
                   q1, q2 being Point of N such that
A43:         uu = [p1,q1] & [x1,x2] = [p2,q2] and
A44:         (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;
            u1 = p1 & u2 = q1 & x1 = p2 & x2 = q2 by A37,A43,ZFMISC_1:33;
          then dist(p1,p2) < r & dist(q1,q2) < r by A40,A41,METRIC_1:12;
          then (the distance of M).(p1,p2) < r &
            (the distance of N).(q1,q2) < r by METRIC_1:def 1;
          then max ((the distance of M).(p1,p2),(the distance of N).(q1,q2)) <
r
            by SQUARE_1:49;
          then dist(uu,[x1,x2]) < r by A44,METRIC_1:def 1;
          then x in Ball(uu,r) by A42,METRIC_1:12;
          hence x in Y by A34;
        end;
          B1 is open & B2 is open by TOPMETR:21;
        then [:B1,B2:] in Base-Appr Y by A30,A39;
        hence u in union Base-Appr Y by A38,TARSKI:def 4;
      end;
        Base-Appr Y c= { [:X1,Y1:] where X1 is Subset of S,
                                       Y1 is Subset of T :
        X1 in the topology of S & Y1 in the topology of T}
      proof
        let A be set;
        assume A in Base-Appr Y;
        then consider X1 being Subset of S, Y1 being Subset of T such that
A45:       A = [:X1,Y1:] and [:X1,Y1:] c= Y and
A46:       X1 is open & Y1 is open by A30;
          X1 in the topology of S & Y1 in
 the topology of T by A46,PRE_TOPC:def 5;
        hence thesis by A45;
      end;
      hence X in the topology of [:S,T:] by A1,A31;
    end;
    hence thesis by A5;
  end;

theorem
   the carrier of M = the carrier of N &
 (for m being Point of M, n being Point of N, r being Real st r > 0 & m = n
   ex r1 being Real st r1 > 0 & Ball(n,r1) c= Ball(m,r)) &
 (for m being Point of M, n being Point of N, r being Real st r > 0 & m = n
   ex r1 being 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 being Point of M, n being Point of N, r being Real st r > 0 & m = n
      ex r1 being Real st r1 > 0 & Ball(n,r1) c= Ball(m,r) and
A3:  for m being Point of M, n being Point of N, r being Real st r > 0 & m = n
      ex r1 being Real st r1 > 0 & Ball(m,r1) c= Ball(n,r);
A4: TopSpaceMetr M = TopStruct (#the carrier of M, Family_open_set M#) &
      TopSpaceMetr N = TopStruct (#the carrier of N, Family_open_set N#)
        by PCOMPS_1:def 6;
      Family_open_set M = Family_open_set N
    proof
      thus Family_open_set M c= Family_open_set N
      proof
        let X be set;
        assume
A5:       X in Family_open_set M;
          for n being Point of N st n in X
         ex r being Real st r > 0 & Ball(n,r) c= X
        proof
          let n be Point of N such that
A6:         n in X;
          reconsider m = n as Point of M by A1;
          consider r being Real such that
A7:         r > 0 and
A8:           Ball(m,r) c= X by A5,A6,PCOMPS_1:def 5;
          consider r1 being Real such that
A9:         r1 > 0 & Ball(n,r1) c= Ball(m,r) by A2,A7;
          take r1;
          thus thesis by A8,A9,XBOOLE_1:1;
        end;
        hence X in Family_open_set N by A1,A5,PCOMPS_1:def 5;
      end;
      let X be set;
      assume
A10:     X in Family_open_set N;
        for m being Point of M st m in X
       ex r being Real st r > 0 & Ball(m,r) c= X
      proof
        let m be Point of M such that
A11:       m in X;
        reconsider n = m as Point of N by A1;
        consider r being Real such that
A12:       r > 0 and
A13:       Ball(n,r) c= X by A10,A11,PCOMPS_1:def 5;
        consider r1 being Real such that
A14:       r1 > 0 & Ball(m,r1) c= Ball(n,r) by A3,A12;
        take r1;
        thus thesis by A13,A14,XBOOLE_1:1;
      end;
      hence X in Family_open_set M by A1,A10,PCOMPS_1:def 5;
    end;
    hence thesis by A1,A4;
  end;

theorem
   [:TOP-REAL i,TOP-REAL j:], TOP-REAL (i+j) are_homeomorphic
  proof
      TOP-REAL i = TopSpaceMetr Euclid i & TOP-REAL j = TopSpaceMetr Euclid j
      by EUCLID:def 8;
then A1: [:TOP-REAL i,TOP-REAL j:] = TopSpaceMetr max-Prod2(Euclid i,Euclid j)
      by Th25;
      TopSpaceMetr max-Prod2(Euclid i,Euclid j), TopSpaceMetr Euclid (i+j)
     are_homeomorphic
    proof
      set ci = the carrier of Euclid i,
          cj = the carrier of Euclid j,
          cij = the carrier of Euclid (i+j);
A2:   Euclid (i+j) = MetrStruct(#REAL (i+j),Pitag_dist (i+j)#)
        by EUCLID:def 7;
A3:   Euclid i = MetrStruct(#REAL i,Pitag_dist i#) by EUCLID:def 7;
A4:   Euclid j = MetrStruct(#REAL j,Pitag_dist j#) by EUCLID:def 7;
defpred P[Element of ci,Element of cj,set] means
 ex fi, fj being FinSequence of REAL st fi = $1 & fj = $2 & $3 = fi ^ fj;
A5:   for x being Element of ci, y being Element of cj
       ex u being Element of cij st P[x,y,u]
      proof
        let x be Element of ci,
            y be Element of cj;
A6:     x is Element of REAL i & y is Element of REAL j by SPPOL_1:18;
        then reconsider fi = x, fj = y as FinSequence of REAL;
          fi is Element of i-tuples_on REAL &
         fj is Element of j-tuples_on REAL by A6,EUCLID:def 1;
        then fi ^ fj is Element of (i+j)-tuples_on REAL by FINSEQ_2:127;
        then reconsider u = fi ^ fj as Element of cij by A2,EUCLID:def 1;
        take u;
        thus P[x,y,u];
      end;
      consider f being Function of [:ci,cj:], cij such that
A7:     for x being Element of ci,
            y being Element of cj holds P[x,y,f. [x,y]] from FuncEx2D(A5);
A8:   [:ci,cj:] = the carrier of max-Prod2(Euclid i,Euclid j) by Def1;
A9:   the carrier of TopSpaceMetr Euclid (i+j) = cij by TOPMETR:16;
A10:   the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j) =
       the carrier of max-Prod2(Euclid i,Euclid j) by TOPMETR:16;
      then reconsider f as map of TopSpaceMetr max-Prod2(Euclid i,Euclid j),
       TopSpaceMetr Euclid (i+j) by A8,A9;
      take f;
A11:   dom f = the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j)
        by FUNCT_2:def 1;
      hence dom f = [#]
TopSpaceMetr max-Prod2(Euclid i,Euclid j) by PRE_TOPC:12;
      thus
A12:     rng f = [#]TopSpaceMetr Euclid (i+j)
      proof
          rng f c= the carrier of TopSpaceMetr Euclid (i+j)
        by RELSET_1:12;
        hence rng f c= [#]TopSpaceMetr Euclid (i+j) by PRE_TOPC:12;
        let y be set;
        assume
A13:       y in [#]TopSpaceMetr Euclid (i+j);
        then reconsider k = y as Element of REAL (i+j) by A2,TOPMETR:16;
          len k = i + j by A9,A13,Th19;
        then consider g, h being FinSequence of REAL such that
A14:       len g = i & len h = j and
A15:       k = g^h by FINSEQ_2:26;
A16:     g in ci & h in cj by A14,Th17;
then A17:     ex fi, fj being FinSequence of REAL st fi = g & fj = h &
         f. [g,h] = fi ^ fj by A7;
          [g,h] in [:ci,cj:] by A16,ZFMISC_1:106;
        then [g,h] in dom f by FUNCT_2:def 1;
        hence thesis by A15,A17,FUNCT_1:def 5;
      end;
      thus
A18:     f is one-to-one
      proof
        let x1, x2 be set;
        assume x1 in dom f;
        then consider x1a, x1b being set such that
A19:       x1a in ci & x1b in cj and
A20:       x1 = [x1a,x1b] by A8,A10,A11,ZFMISC_1:def 2;
        assume x2 in dom f;
        then consider x2a, x2b being set such that
A21:       x2a in ci & x2b in cj and
A22:       x2 = [x2a,x2b] by A8,A10,A11,ZFMISC_1:def 2;
        consider fi1, fj1 being FinSequence of REAL such that
A23:       fi1 = x1a & fj1 = x1b & f. [x1a,x1b] = fi1 ^ fj1 by A7,A19;
        consider fi2, fj2 being FinSequence of REAL such that
A24:       fi2 = x2a & fj2 = x2b & f. [x2a,x2b] = fi2 ^ fj2 by A7,A21;
          len fi1 = i & len fj1 = j by A19,A23,Th19;
then A25:     len fi1 = len fi2 & len fj1 = len fj2 by A21,A24,Th19;
        assume f.x1 = f.x2;
        then fi1 = fi2 & fj1 = fj2 by A20,A22,A23,A24,A25,Th6;
        hence x1 = x2 by A20,A22,A23,A24;
      end;
        for P being 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) by PRE_TOPC:def 5;
then A26:     P in Family_open_set Euclid (i+j) by TOPMETR:16;
A27:     f"P is Subset of max-Prod2(Euclid i,Euclid j)
          by TOPMETR:16;
          for x being Point of max-Prod2(Euclid i,Euclid j) st x in f"P
          ex r being Real st r > 0 & Ball(x,r) c= f"P
        proof
          let x be Point of max-Prod2(Euclid i,Euclid j);
          assume
A28:         x in f"P;
          then f.x in the carrier of TopSpaceMetr Euclid (i+j) by FUNCT_2:7;
          then reconsider fx = f.x as Point of Euclid (i+j) by TOPMETR:16;
            f.x in P by A28,FUNCT_2:46;
          then consider r being Real such that
A29:         r > 0 and
A30:         Ball(fx,r) c= P by A26,PCOMPS_1:def 5;
          take r1 = r/2;
          thus r1 > 0 by A29,REAL_2:127;
          let b be set;
          assume
A31:         b in Ball(x,r1);
          then reconsider bb = b as Point of max-Prod2(Euclid i,Euclid j);
          consider b1, x1 being Point of Euclid i,
                   b2, x2 being Point of Euclid j such that
A32:         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;
          consider b1f, b2f being FinSequence of REAL such that
A33:         b1f = b1 & b2f = b2 & f. [b1,b2] = b1f ^ b2f by A7;
          consider x1f, x2f being FinSequence of REAL such that
A34:         x1f = x1 & x2f = x2 & f. [x1,x2] = x1f ^ x2f by A7;
A35:       dist([b1,b2],[x1,x2]) = max (dist(b1,x1),dist(b2,x2)) by Th20;
A36:       dist(bb,x) < r1 by A31,METRIC_1:12;
            bb in the carrier of max-Prod2(Euclid i,Euclid j);
then A37:       bb in the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j)
            by TOPMETR:16;
          then f.bb in the carrier of TopSpaceMetr Euclid (i+j) by FUNCT_2:7;
          then reconsider fb = f.b as Point of Euclid (i+j) by TOPMETR:16;
          reconsider fbb = fb, fxx = fx as Element of REAL (i+j) by A2;
          reconsider b1i = b1, x1i = x1 as Element of REAL i by A3;
          reconsider x2i = x2, b2i = b2 as Element of REAL j by A4;
            dist(b1,x1) <= max (dist(b1,x1),dist(b2,x2)) &
          dist(b2,x2) <= max (dist(b1,x1),dist(b2,x2)) by SQUARE_1:46;
          then dist(b1,x1) < r1 & dist(b2,x2) < r1 by A32,A35,A36,AXIOMS:22;
then A38:       (Pitag_dist i).(b1i,x1i) < r1 & (Pitag_dist j).(b2i,x2i) < r1
            by A3,A4,METRIC_1:def 1;
A39:       len b1f = i & len x1f = i & len b2f = j & len x2f = j by A33,A34,
Th19;
A40:       (Pitag_dist (i+j)).(fbb,fxx) = |.fbb - fxx.| by EUCLID:def 6
            .= sqrt Sum sqr (fbb - fxx) by EUCLID:def 5
            .= sqrt Sum sqr abs (fbb - fxx) by EUCLID:29
            .= sqrt Sum sqr (abs (b1i - x1i) ^ abs (b2i - x2i))
               by A32,A33,A34,A39,Th16
            .= sqrt Sum (sqr abs (b1i - x1i) ^ sqr abs (b2i - x2i)) by Th11
            .= sqrt (Sum sqr abs (b1i - x1i) + Sum sqr abs (b2i - x2i))
               by RVSUM_1:105
            .= sqrt (Sum sqr abs (b1i - x1i) + Sum sqr (b2i - x2i))
               by EUCLID:29
            .= sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
               by EUCLID:29;
            0 <= Sum sqr (b1i - x1i) & 0 <= Sum sqr (b2i - x2i)
            by RVSUM_1:116;
          then sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
            <= sqrt Sum sqr (b1i - x1i) + sqrt Sum sqr (b2i - x2i)
              by TOPREAL6:6;
          then sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
            <= |.b1i - x1i.| + sqrt Sum sqr (b2i - x2i) by EUCLID:def 5;
          then sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
            <= |.b1i - x1i.| + |.b2i - x2i.| by EUCLID:def 5;
          then sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
            <= (Pitag_dist i).(b1i,x1i) + |.b2i - x2i.| by EUCLID:def 6;
then A41:       sqrt (Sum sqr (b1i - x1i) + Sum sqr (b2i - x2i))
            <= (Pitag_dist i).(b1i,x1i) + (Pitag_dist j).(b2i,x2i)
               by EUCLID:def 6;
            (Pitag_dist i).(b1i,x1i) + (Pitag_dist j).(b2i,x2i) < r1 + r1
            by A38,REAL_1:67;
          then (Pitag_dist (i+j)).(fbb,fxx) < r1 + r1 by A40,A41,AXIOMS:22;
          then (Pitag_dist (i+j)).(fbb,fxx) < r by XCMPLX_1:66;
          then dist(fb,fx) < r by A2,METRIC_1:def 1;
          then f.b in Ball(fx,r) by METRIC_1:12;
          hence b in f"P by A30,A37,FUNCT_2:46;
        end;
        then f"P in Family_open_set max-Prod2(Euclid i,Euclid j)
          by A27,PCOMPS_1:def 5;
        hence f"P in the topology of TopSpaceMetr max-Prod2(Euclid i,Euclid j)
          by TOPMETR:16;
      end;
      hence f is continuous by TOPS_2:55;
        for P being 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)
          by PRE_TOPC:def 5;
then A42:     P in Family_open_set max-Prod2(Euclid i,Euclid j) by TOPMETR:16;
A43:     f.:P is Subset of Euclid (i+j) by TOPMETR:16;
          for x being Point of Euclid (i+j) st x in f.:P
          ex r being 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 being set such that
A44:         a in the carrier of TopSpaceMetr max-Prod2(Euclid i,Euclid j) and
A45:         a in P and
A46:         x = f.a by FUNCT_2:115;
          reconsider a as Point of max-Prod2(Euclid i,Euclid j)
            by A44,TOPMETR:16;
          consider r being Real such that
A47:         r > 0 and
A48:         Ball(a,r) c= P by A42,A45,PCOMPS_1:def 5;
          take r;
          thus r > 0 by A47;
          let b be set;
          assume
A49:         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) by SPPOL_1:18;
            dist(bb,x) < r by A49,METRIC_1:12;
then A50:       (the distance of Euclid (i+j)).(bb,x) < r by METRIC_1:def 1;
          reconsider k = bb as Element of REAL (i+j) by A2;
            len k = i + j by Th19;
          then consider g, h being FinSequence of REAL such that
A51:         len g = i and
A52:         len h = j and
A53:         k = g^h by FINSEQ_2:26;
          consider p, q being set such that
A54:         p in ci and
A55:         q in cj and
A56:         a = [p,q] by A8,ZFMISC_1:def 2;
          reconsider p as Element of ci by A54;
          reconsider q as Element of cj by A55;
          consider fi, fj being FinSequence of REAL such that
A57:         fi = p & fj = q and
A58:         f. [p,q] = fi ^ fj by A7;
          reconsider gg = g as Point of Euclid i by A51,Th17;
          reconsider hh = h as Point of Euclid j by A52,Th17;
          consider g, h being FinSequence of REAL such that
A59:         g = gg & h = hh and
A60:         f. [gg,hh] = g ^ h by A7;
          reconsider gg2 = gg, a12 = a`1 as Element of REAL i by SPPOL_1:18;
          reconsider hh2 = hh, a22 = a`2 as Element of REAL j by SPPOL_1:18;
A61:       len g = i & len fi = i & len h = j & len fj = j by A57,A59,Th19;
            |.bb2-xx2.| < r by A2,A50,EUCLID:def 6;
          then sqrt Sum sqr (bb2-xx2) < r by EUCLID:def 5;
          then sqrt Sum sqr abs (bb2-xx2) < r by EUCLID:29;
          then sqrt Sum sqr (abs(g-fi) ^ abs(h-fj)) < r
            by A46,A53,A56,A58,A59,A61,Th16;
          then sqrt Sum (sqr abs (g-fi) ^ sqr abs (h-fj)) < r by Th11;
then A62:      sqrt (Sum sqr abs (g-fi) + Sum sqr abs (h-fj)) < r by RVSUM_1:
105;
A63:       dist([gg,hh],[a`1,a`2]) = max (dist(gg,a`1),dist(hh,a`2)) by Th20;
A64:       a12 = p & a22 = q by A56,MCART_1:7;
A65:       0 <= Sum sqr abs (gg2-a12) & 0 <= Sum
 sqr abs (hh2-a22) by RVSUM_1:116;
            0 <= Sum sqr abs (g-fi) & 0 <= Sum
 sqr abs (h-fj) by RVSUM_1:116;
          then Sum sqr abs (gg2-a12) + 0 <= Sum sqr abs (g-fi) + Sum
 sqr abs (h-fj) &
           Sum sqr abs (hh2-a22) + 0 <= Sum sqr abs (g-fi) + Sum sqr abs (h-fj)
            by A57,A59,A64,REAL_1:55;
          then sqrt Sum sqr abs (gg2-a12) <= sqrt (Sum sqr abs (g-fi) +
            Sum sqr abs (h-fj)) &
          sqrt Sum sqr abs (hh2-a22) <= sqrt (Sum sqr abs (g-fi) +
            Sum sqr abs (h-fj)) by A65,SQUARE_1:94;
          then sqrt Sum sqr abs (gg2-a12) < r & sqrt Sum sqr abs (hh2-a22) < r
           by A62,AXIOMS:22;
          then sqrt Sum sqr (gg2-a12) < r & sqrt Sum sqr (hh2-a22) < r
           by EUCLID:29;
          then |.gg2-a12.| < r & |.hh2-a22.| < r by EUCLID:def 5;
          then (Pitag_dist i).(gg2,a12) < r &
           (Pitag_dist j).(hh2,a22) < r by EUCLID:def 6;
then A66:       dist(gg,a`1) < r & dist(hh,a`2) < r by A3,A4,METRIC_1:def 1;
            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 SQUARE_1:49;
          then dist([gg,hh],a) < r by A8,A63,A66,MCART_1:23;
          then [g,h] in Ball(a,r) by A59,METRIC_1:12;
          then [g,h] in P by A48;
          hence b in f.:P by A53,A59,A60,FUNCT_2:43;
        end;
        then f.:P in Family_open_set Euclid (i+j) by A43,PCOMPS_1:def 5;
        then f.:P in the topology of TopSpaceMetr Euclid (i+j) by TOPMETR:16;
        hence f""P in the topology of TopSpaceMetr Euclid (i+j)
          by A12,A18,TOPS_2:67;
      end;
      hence f" is continuous by TOPS_2:55;
    end;
    hence thesis by A1,EUCLID:def 8;
  end;

Back to top