Copyright (c) 1999 Association of Mizar Users
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;