:: TOPREAL7 semantic presentation begin theorem Th1: :: TOPREAL7:1 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; ::_thesis: max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d)) ( b <= max (a,b) & d <= max (c,d) ) by XXREAL_0:25; then A1: b + d <= (max (a,b)) + (max (c,d)) by XREAL_1:7; ( a <= max (a,b) & c <= max (c,d) ) by XXREAL_0:25; then a + c <= (max (a,b)) + (max (c,d)) by XREAL_1:7; hence max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d)) by A1, XXREAL_0:28; ::_thesis: verum end; theorem Th2: :: TOPREAL7:2 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; ::_thesis: ( a <= b + c & d <= e + f implies max (a,d) <= (max (b,e)) + (max (c,f)) ) assume ( a <= b + c & d <= e + f ) ; ::_thesis: max (a,d) <= (max (b,e)) + (max (c,f)) then A1: max (a,d) <= max ((b + c),(e + f)) by XXREAL_0:26; max ((b + c),(e + f)) <= (max (b,e)) + (max (c,f)) by Th1; hence max (a,d) <= (max (b,e)) + (max (c,f)) by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: TOPREAL7:3 for f, g being FinSequence holds dom g c= dom (f ^ g) proof let f, g be FinSequence; ::_thesis: dom g c= dom (f ^ g) len g <= (len f) + (len g) by NAT_1:11; then Seg (len g) c= Seg ((len f) + (len g)) by FINSEQ_1:5; then dom g c= Seg ((len f) + (len g)) by FINSEQ_1:def_3; hence dom g c= dom (f ^ g) by FINSEQ_1:def_7; ::_thesis: verum end; theorem Th4: :: TOPREAL7:4 for i being Nat for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds i - (len f) in dom g proof let i be Nat; ::_thesis: for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds i - (len f) in dom g let f, g be FinSequence; ::_thesis: ( len f < i & i <= (len f) + (len g) implies i - (len f) in dom g ) assume that A1: len f < i and A2: i <= (len f) + (len g) ; ::_thesis: i - (len f) in dom g A3: i - (len f) is Element of NAT by A1, INT_1:5; A4: i - (len f) <= ((len f) + (len g)) - (len f) by A2, XREAL_1:9; i - (len f) > (len f) - (len f) by A1, XREAL_1:14; then 1 <= i - (len f) by A3, NAT_1:14; hence i - (len f) in dom g by A3, A4, FINSEQ_3:25; ::_thesis: verum end; theorem Th5: :: TOPREAL7:5 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; ::_thesis: ( f ^ g = h ^ k & len f = len h & len g = len k implies ( f = h & g = k ) ) assume that A1: f ^ g = h ^ k and A2: len f = len h and A3: len g = len k ; ::_thesis: ( f = h & g = k ) A4: for i being Nat st 1 <= i & i <= len f holds f . i = h . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = h . i ) assume A5: ( 1 <= i & i <= len f ) ; ::_thesis: f . i = h . i then A6: i in dom h by A2, FINSEQ_3:25; i in dom f by A5, FINSEQ_3:25; hence f . i = (f ^ g) . i by FINSEQ_1:def_7 .= h . i by A1, A6, FINSEQ_1:def_7 ; ::_thesis: verum end; for i being Nat st 1 <= i & i <= len g holds g . i = k . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len g implies g . i = k . i ) assume A7: ( 1 <= i & i <= len g ) ; ::_thesis: g . i = k . i then A8: i in dom k by A3, FINSEQ_3:25; i in dom g by A7, FINSEQ_3:25; hence g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def_7 .= k . i by A1, A2, A8, FINSEQ_1:def_7 ; ::_thesis: verum end; hence ( f = h & g = k ) by A2, A3, A4, FINSEQ_1:14; ::_thesis: verum end; theorem Th6: :: TOPREAL7:6 for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds ( len (f + g) = len f & dom (f + g) = dom f ) proof let f, g be FinSequence of REAL ; ::_thesis: ( ( len f = len g or dom f = dom g ) implies ( len (f + g) = len f & dom (f + g) = dom f ) ) reconsider f1 = f as Element of (len f) -tuples_on REAL by FINSEQ_2:92; assume ( len f = len g or dom f = dom g ) ; ::_thesis: ( len (f + g) = len f & dom (f + g) = dom f ) then len f = len g by FINSEQ_3:29; then reconsider g1 = g as Element of (len f) -tuples_on REAL by FINSEQ_2:92; f1 + g1 is Element of (len f) -tuples_on REAL ; hence len (f + g) = len f by CARD_1:def_7; ::_thesis: dom (f + g) = dom f hence dom (f + g) = dom f by FINSEQ_3:29; ::_thesis: verum end; theorem Th7: :: TOPREAL7:7 for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds ( len (f - g) = len f & dom (f - g) = dom f ) proof let f, g be FinSequence of REAL ; ::_thesis: ( ( len f = len g or dom f = dom g ) implies ( len (f - g) = len f & dom (f - g) = dom f ) ) reconsider f1 = f as Element of (len f) -tuples_on REAL by FINSEQ_2:92; assume ( len f = len g or dom f = dom g ) ; ::_thesis: ( len (f - g) = len f & dom (f - g) = dom f ) then len f = len g by FINSEQ_3:29; then reconsider g1 = g as Element of (len f) -tuples_on REAL by FINSEQ_2:92; f1 - g1 is Element of (len f) -tuples_on REAL ; hence len (f - g) = len f by CARD_1:def_7; ::_thesis: dom (f - g) = dom f hence dom (f - g) = dom f by FINSEQ_3:29; ::_thesis: verum end; theorem Th8: :: TOPREAL7:8 for f being FinSequence of REAL holds ( len f = len (sqr f) & dom f = dom (sqr f) ) by RVSUM_1:143; theorem Th9: :: TOPREAL7:9 for f being FinSequence of REAL holds ( len f = len (abs f) & dom f = dom (abs f) ) proof let f be FinSequence of REAL ; ::_thesis: ( len f = len (abs f) & dom f = dom (abs f) ) ( rng f c= REAL & dom absreal = REAL ) by FUNCT_2:def_1; hence len f = len (abs f) by FINSEQ_2:29; ::_thesis: dom f = dom (abs f) hence dom f = dom (abs f) by FINSEQ_3:29; ::_thesis: verum end; theorem Th10: :: TOPREAL7:10 for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g) by RVSUM_1:144; theorem :: TOPREAL7:11 for f, g being FinSequence of REAL holds abs (f ^ g) = (abs f) ^ (abs g) proof let f, g be FinSequence of REAL ; ::_thesis: abs (f ^ g) = (abs f) ^ (abs g) A1: ( len g = len (abs g) & len (f ^ g) = (len f) + (len g) ) by Th9, FINSEQ_1:22; A2: len (abs (f ^ g)) = len (f ^ g) by Th9; A3: len f = len (abs f) by Th9; A4: for i being Nat st 1 <= i & i <= len (abs (f ^ g)) holds (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs (f ^ g)) implies (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i ) assume that A5: 1 <= i and A6: i <= len (abs (f ^ g)) ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i reconsider i1 = i as Element of NAT by ORDINAL1:def_12; A7: i in dom (f ^ g) by A2, A5, A6, FINSEQ_3:25; percases ( i in dom f or not i in dom f ) ; supposeA8: i in dom f ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i then A9: i in dom (abs f) by Th9; thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13 .= absreal . (f . i) by A8, FINSEQ_1:def_7 .= abs (f . i1) by EUCLID:def_2 .= (abs f) . i1 by A9, TOPREAL6:12 .= ((abs f) ^ (abs g)) . i by A9, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose not i in dom f ; ::_thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i then A10: len f < i by A5, FINSEQ_3:25; then reconsider j = i1 - (len f) as Element of NAT by INT_1:5; A11: i <= len (f ^ g) by A6, Th9; then A12: j in dom (abs g) by A1, A10, Th4; A13: i <= len ((abs f) ^ (abs g)) by A3, A1, A2, A6, FINSEQ_1:22; thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13 .= absreal . (g . j) by A10, A11, FINSEQ_1:24 .= abs (g . j) by EUCLID:def_2 .= (abs g) . j by A12, TOPREAL6:12 .= ((abs f) ^ (abs g)) . i by A3, A10, A13, FINSEQ_1:24 ; ::_thesis: verum end; end; end; len (abs (f ^ g)) = len ((abs f) ^ (abs g)) by A3, A1, A2, FINSEQ_1:22; hence abs (f ^ g) = (abs f) ^ (abs g) by A4, FINSEQ_1:14; ::_thesis: verum end; theorem :: TOPREAL7:12 for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) proof let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) ) assume that A1: len f = len h and A2: len g = len k ; ::_thesis: sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22; A5: len (sqr ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th8 .= len (f ^ g) by A1, A2, A3, A4, Th6 .= (len (f + h)) + (len g) by A1, A3, Th6 .= (len (f + h)) + (len (g + k)) by A2, Th6 .= (len (sqr (f + h))) + (len (g + k)) by Th8 .= (len (sqr (f + h))) + (len (sqr (g + k))) by Th8 .= len ((sqr (f + h)) ^ (sqr (g + k))) by FINSEQ_1:22 ; for i being Nat st 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) holds (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) implies (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i ) assume that A6: 1 <= i and A7: i <= len (sqr ((f ^ g) + (h ^ k))) ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i i in dom (sqr ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25; then A8: i in dom ((f ^ g) + (h ^ k)) by Th8; percases ( i in dom f or not i in dom f ) ; supposeA9: i in dom f ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i then A10: i in dom (f + h) by A1, Th6; then A11: i in dom (sqr (f + h)) by Th8; A12: i in dom h by A1, A9, FINSEQ_3:29; thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11 .= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def_1 .= ((f . i) + ((h ^ k) . i)) ^2 by A9, FINSEQ_1:def_7 .= ((f . i) + (h . i)) ^2 by A12, FINSEQ_1:def_7 .= ((f + h) . i) ^2 by A10, VALUED_1:def_1 .= (sqr (f + h)) . i by VALUED_1:11 .= ((sqr (f + h)) ^ (sqr (g + k))) . i by A11, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose not i in dom f ; ::_thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i then A13: len f < i by A6, FINSEQ_3:25; then reconsider j = i - (len f) as Element of NAT by INT_1:5; A14: len (f + h) < i by A1, A13, Th6; then A15: len (sqr (f + h)) < i by Th8; i <= len ((f ^ g) + (h ^ k)) by A7, Th8; then A16: i <= len (f ^ g) by A1, A2, A3, A4, Th6; then i <= (len (f + h)) + (len g) by A1, A3, Th6; then i <= (len (f + h)) + (len (g + k)) by A2, Th6; then i - (len (f + h)) in dom (g + k) by A14, Th4; then A17: j in dom (g + k) by A1, Th6; len f = len (f + h) by A1, Th6; then A18: j = i - (len (sqr (f + h))) by Th8; thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11 .= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def_1 .= ((g . j) + ((h ^ k) . i)) ^2 by A13, A16, FINSEQ_1:24 .= ((g . j) + (k . j)) ^2 by A1, A2, A3, A4, A13, A16, FINSEQ_1:24 .= ((g + k) . j) ^2 by A17, VALUED_1:def_1 .= (sqr (g + k)) . j by VALUED_1:11 .= ((sqr (f + h)) ^ (sqr (g + k))) . i by A5, A7, A15, A18, FINSEQ_1:24 ; ::_thesis: verum end; end; end; hence sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) by A5, FINSEQ_1:14; ::_thesis: verum end; theorem :: TOPREAL7:13 for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) proof let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) ) assume that A1: len f = len h and A2: len g = len k ; ::_thesis: abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22; A5: len (abs ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th9 .= len (f ^ g) by A1, A2, A3, A4, Th6 .= (len (f + h)) + (len g) by A1, A3, Th6 .= (len (f + h)) + (len (g + k)) by A2, Th6 .= (len (abs (f + h))) + (len (g + k)) by Th9 .= (len (abs (f + h))) + (len (abs (g + k))) by Th9 .= len ((abs (f + h)) ^ (abs (g + k))) by FINSEQ_1:22 ; for i being Nat st 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) holds (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) implies (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i ) assume that A6: 1 <= i and A7: i <= len (abs ((f ^ g) + (h ^ k))) ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i reconsider i1 = i as Element of NAT by ORDINAL1:def_12; A8: i in dom (abs ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25; then A9: i in dom ((f ^ g) + (h ^ k)) by Th9; percases ( i in dom f or not i in dom f ) ; supposeA10: i in dom f ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i then A11: i in dom h by A1, FINSEQ_3:29; A12: i in dom (f + h) by A1, A10, Th6; then A13: i in dom (abs (f + h)) by Th9; thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:12 .= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def_1 .= abs ((f . i) + ((h ^ k) . i)) by A10, FINSEQ_1:def_7 .= abs ((f . i) + (h . i)) by A11, FINSEQ_1:def_7 .= abs ((f + h) . i1) by A12, VALUED_1:def_1 .= (abs (f + h)) . i1 by A13, TOPREAL6:12 .= ((abs (f + h)) ^ (abs (g + k))) . i by A13, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose not i in dom f ; ::_thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i then A14: len f < i by A6, FINSEQ_3:25; then reconsider j = i - (len f) as Element of NAT by INT_1:5; A15: len (f + h) < i by A1, A14, Th6; then A16: len (abs (f + h)) < i by Th9; i <= len ((f ^ g) + (h ^ k)) by A7, Th9; then A17: i <= len (f ^ g) by A1, A2, A3, A4, Th6; then i <= (len (f + h)) + (len g) by A1, A3, Th6; then i <= (len (f + h)) + (len (g + k)) by A2, Th6; then i - (len (f + h)) in dom (g + k) by A15, Th4; then A18: j in dom (g + k) by A1, Th6; then A19: j in dom (abs (g + k)) by Th9; len f = len (f + h) by A1, Th6; then A20: j = i - (len (abs (f + h))) by Th9; thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:12 .= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def_1 .= abs ((g . j) + ((h ^ k) . i)) by A14, A17, FINSEQ_1:24 .= abs ((g . j) + (k . j)) by A1, A2, A3, A4, A14, A17, FINSEQ_1:24 .= abs ((g + k) . j) by A18, VALUED_1:def_1 .= (abs (g + k)) . j by A19, TOPREAL6:12 .= ((abs (f + h)) ^ (abs (g + k))) . i by A5, A7, A16, A20, FINSEQ_1:24 ; ::_thesis: verum end; end; end; hence abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) by A5, FINSEQ_1:14; ::_thesis: verum end; theorem :: TOPREAL7:14 for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) proof let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) ) assume that A1: len f = len h and A2: len g = len k ; ::_thesis: sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22; A5: len (sqr ((f ^ g) - (h ^ k))) = len ((f ^ g) - (h ^ k)) by Th8 .= len (f ^ g) by A1, A2, A3, A4, Th7 .= (len (f - h)) + (len g) by A1, A3, Th7 .= (len (f - h)) + (len (g - k)) by A2, Th7 .= (len (sqr (f - h))) + (len (g - k)) by Th8 .= (len (sqr (f - h))) + (len (sqr (g - k))) by Th8 .= len ((sqr (f - h)) ^ (sqr (g - k))) by FINSEQ_1:22 ; for i being Nat st 1 <= i & i <= len (sqr ((f ^ g) - (h ^ k))) holds (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr ((f ^ g) - (h ^ k))) implies (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i ) assume that A6: 1 <= i and A7: i <= len (sqr ((f ^ g) - (h ^ k))) ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i i in dom (sqr ((f ^ g) - (h ^ k))) by A6, A7, FINSEQ_3:25; then A8: i in dom ((f ^ g) - (h ^ k)) by Th8; percases ( i in dom f or not i in dom f ) ; supposeA9: i in dom f ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i then A10: i in dom (f - h) by A1, Th7; then A11: i in dom (sqr (f - h)) by Th8; A12: i in dom h by A1, A9, FINSEQ_3:29; thus (sqr ((f ^ g) - (h ^ k))) . i = (((f ^ g) - (h ^ k)) . i) ^2 by VALUED_1:11 .= (((f ^ g) . i) - ((h ^ k) . i)) ^2 by A8, VALUED_1:13 .= ((f . i) - ((h ^ k) . i)) ^2 by A9, FINSEQ_1:def_7 .= ((f . i) - (h . i)) ^2 by A12, FINSEQ_1:def_7 .= ((f - h) . i) ^2 by A10, VALUED_1:13 .= (sqr (f - h)) . i by VALUED_1:11 .= ((sqr (f - h)) ^ (sqr (g - k))) . i by A11, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose not i in dom f ; ::_thesis: (sqr ((f ^ g) - (h ^ k))) . i = ((sqr (f - h)) ^ (sqr (g - k))) . i then A13: len f < i by A6, FINSEQ_3:25; then reconsider j = i - (len f) as Element of NAT by INT_1:5; A14: len (f - h) < i by A1, A13, Th7; then A15: len (sqr (f - h)) < i by Th8; i <= len ((f ^ g) - (h ^ k)) by A7, Th8; then A16: i <= len (f ^ g) by A1, A2, A3, A4, Th7; then i <= (len (f - h)) + (len g) by A1, A3, Th7; then i <= (len (f - h)) + (len (g - k)) by A2, Th7; then i - (len (f - h)) in dom (g - k) by A14, Th4; then A17: j in dom (g - k) by A1, Th7; len f = len (f - h) by A1, Th7; then A18: j = i - (len (sqr (f - h))) by Th8; thus (sqr ((f ^ g) - (h ^ k))) . i = (((f ^ g) - (h ^ k)) . i) ^2 by VALUED_1:11 .= (((f ^ g) . i) - ((h ^ k) . i)) ^2 by A8, VALUED_1:13 .= ((g . j) - ((h ^ k) . i)) ^2 by A13, A16, FINSEQ_1:24 .= ((g . j) - (k . j)) ^2 by A1, A2, A3, A4, A13, A16, FINSEQ_1:24 .= ((g - k) . j) ^2 by A17, VALUED_1:13 .= (sqr (g - k)) . j by VALUED_1:11 .= ((sqr (f - h)) ^ (sqr (g - k))) . i by A5, A7, A15, A18, FINSEQ_1:24 ; ::_thesis: verum end; end; end; hence sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k)) by A5, FINSEQ_1:14; ::_thesis: verum end; theorem Th15: :: TOPREAL7:15 for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) proof let f, h, g, k be FinSequence of REAL ; ::_thesis: ( len f = len h & len g = len k implies abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) ) assume that A1: len f = len h and A2: len g = len k ; ::_thesis: abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22; A5: len (abs ((f ^ g) - (h ^ k))) = len ((f ^ g) - (h ^ k)) by Th9 .= len (f ^ g) by A1, A2, A3, A4, Th7 .= (len (f - h)) + (len g) by A1, A3, Th7 .= (len (f - h)) + (len (g - k)) by A2, Th7 .= (len (abs (f - h))) + (len (g - k)) by Th9 .= (len (abs (f - h))) + (len (abs (g - k))) by Th9 .= len ((abs (f - h)) ^ (abs (g - k))) by FINSEQ_1:22 ; for i being Nat st 1 <= i & i <= len (abs ((f ^ g) - (h ^ k))) holds (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (abs ((f ^ g) - (h ^ k))) implies (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i ) assume that A6: 1 <= i and A7: i <= len (abs ((f ^ g) - (h ^ k))) ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i A8: i in dom (abs ((f ^ g) - (h ^ k))) by A6, A7, FINSEQ_3:25; then A9: i in dom ((f ^ g) - (h ^ k)) by Th9; percases ( i in dom f or not i in dom f ) ; supposeA10: i in dom f ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i reconsider i1 = i as Element of NAT by ORDINAL1:def_12; A11: i in dom h by A1, A10, FINSEQ_3:29; A12: i in dom (f - h) by A1, A10, Th7; then A13: i in dom (abs (f - h)) by Th9; thus (abs ((f ^ g) - (h ^ k))) . i = abs (((f ^ g) - (h ^ k)) . i1) by A8, TOPREAL6:12 .= abs (((f ^ g) . i) - ((h ^ k) . i)) by A9, VALUED_1:13 .= abs ((f . i) - ((h ^ k) . i)) by A10, FINSEQ_1:def_7 .= abs ((f . i) - (h . i)) by A11, FINSEQ_1:def_7 .= abs ((f - h) . i1) by A12, VALUED_1:13 .= (abs (f - h)) . i1 by A13, TOPREAL6:12 .= ((abs (f - h)) ^ (abs (g - k))) . i by A13, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA14: not i in dom f ; ::_thesis: (abs ((f ^ g) - (h ^ k))) . i = ((abs (f - h)) ^ (abs (g - k))) . i reconsider i1 = i as Element of NAT by ORDINAL1:def_12; A15: len f < i by A6, A14, FINSEQ_3:25; then reconsider j = i - (len f) as Element of NAT by INT_1:5; A16: len (f - h) < i by A1, A15, Th7; then A17: len (abs (f - h)) < i by Th9; i <= len ((f ^ g) - (h ^ k)) by A7, Th9; then A18: i <= len (f ^ g) by A1, A2, A3, A4, Th7; then i <= (len (f - h)) + (len g) by A1, A3, Th7; then i <= (len (f - h)) + (len (g - k)) by A2, Th7; then i - (len (f - h)) in dom (g - k) by A16, Th4; then A19: j in dom (g - k) by A1, Th7; then A20: j in dom (abs (g - k)) by Th9; len f = len (f - h) by A1, Th7; then A21: j = i - (len (abs (f - h))) by Th9; thus (abs ((f ^ g) - (h ^ k))) . i = abs (((f ^ g) - (h ^ k)) . i1) by A8, TOPREAL6:12 .= abs (((f ^ g) . i) - ((h ^ k) . i)) by A9, VALUED_1:13 .= abs ((g . j) - ((h ^ k) . i)) by A15, A18, FINSEQ_1:24 .= abs ((g . j) - (k . j)) by A1, A2, A3, A4, A15, A18, FINSEQ_1:24 .= abs ((g - k) . j) by A19, VALUED_1:13 .= (abs (g - k)) . j by A20, TOPREAL6:12 .= ((abs (f - h)) ^ (abs (g - k))) . i by A5, A7, A17, A21, FINSEQ_1:24 ; ::_thesis: verum end; end; end; hence abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k)) by A5, FINSEQ_1:14; ::_thesis: verum end; theorem Th16: :: TOPREAL7:16 for n being Element of NAT for f being FinSequence of REAL st len f = n holds f in the carrier of (Euclid n) by TOPREAL3:45; theorem :: TOPREAL7:17 for n being Element of NAT for f being FinSequence of REAL st len f = n holds f in the carrier of (TOP-REAL n) by TOPREAL3:46; definition let M, N be non empty MetrStruct ; func max-Prod2 (M,N) -> strict MetrStruct means :Def1: :: TOPREAL7:def 1 ( 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 ex 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 ex b1 being strict MetrStruct st ( the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) proof defpred S1[ set , set , set ] means ex x1, y1 being Point of M ex 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))) ); set C = [: the carrier of M, the carrier of N:]; A1: for x, y being Element of [: the carrier of M, the carrier of N:] ex u being Element of REAL st S1[x,y,u] proof let x, y be Element of [: the carrier of M, the carrier of N:]; ::_thesis: ex u being Element of REAL st S1[x,y,u] set x1 = x `1 ; set x2 = x `2 ; set y1 = y `1 ; set y2 = y `2 ; take max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ; ::_thesis: S1[x,y, max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2))))] take x `1 ; ::_thesis: ex y1 being Point of M ex x2, y2 being Point of N st ( x = [(x `1),x2] & y = [y1,y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),y1)),( the distance of N . (x2,y2))) ) take y `1 ; ::_thesis: ex x2, y2 being Point of N st ( x = [(x `1),x2] & y = [(y `1),y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . (x2,y2))) ) take x `2 ; ::_thesis: ex y2 being Point of N st ( x = [(x `1),(x `2)] & y = [(y `1),y2] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),y2))) ) take y `2 ; ::_thesis: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ) thus ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ) by MCART_1:21; ::_thesis: verum end; consider f being Function of [:[: the carrier of M, the carrier of N:],[: the carrier of M, the carrier of N:]:],REAL such that A2: for x, y being Element of [: the carrier of M, the carrier of N:] holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1); take E = MetrStruct(# [: the carrier of M, the carrier of N:],f #); ::_thesis: ( the carrier of E = [: the carrier of M, the carrier of N:] & ( for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) thus the carrier of E = [: the carrier of M, the carrier of N:] ; ::_thesis: for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) let x, y be Point of E; ::_thesis: ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) 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 ; ::_thesis: ex y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) take y1 ; ::_thesis: ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) take x2 ; ::_thesis: ex y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) take y2 ; ::_thesis: ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) thus ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being strict MetrStruct st the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & the carrier of b2 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b2 ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of b2 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) holds b1 = b2 proof let A, B be strict MetrStruct ; ::_thesis: ( the carrier of A = [: the carrier of M, the carrier of N:] & ( for x, y being Point of A ex x1, y1 being Point of M ex 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))) ) ) & the carrier of B = [: the carrier of M, the carrier of N:] & ( for x, y being Point of B ex x1, y1 being Point of M ex 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))) ) ) implies A = B ) assume 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 ex 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 ex 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))) ) ; ::_thesis: A = B set f = the distance of A; set g = the distance of B; for a, b being set st a in the carrier of A & b in the carrier of A holds the distance of A . (a,b) = the distance of B . (a,b) proof let a, b be set ; ::_thesis: ( a in the carrier of A & b in the carrier of A implies the distance of A . (a,b) = the distance of B . (a,b) ) assume A8: ( a in the carrier of A & b in the carrier of A ) ; ::_thesis: the distance of A . (a,b) = the distance of B . (a,b) then consider x1, y1 being Point of M, x2, y2 being Point of N such that A9: a = [x1,x2] and A10: b = [y1,y2] and A11: the distance of A . (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 A12: a = [m1,m2] and A13: b = [n1,n2] and A14: the distance of B . (a,b) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by A4, A6, A7, A8; A15: y1 = n1 by A10, A13, XTUPLE_0:1; ( x1 = m1 & x2 = m2 ) by A9, A12, XTUPLE_0:1; hence the distance of A . (a,b) = the distance of B . (a,b) by A10, A11, A13, A14, A15, XTUPLE_0:1; ::_thesis: verum end; hence A = B by A4, A6, BINOP_1:1; ::_thesis: verum end; end; :: deftheorem Def1 defines max-Prod2 TOPREAL7:def_1_:_ for M, N being non empty MetrStruct for b3 being strict MetrStruct holds ( b3 = max-Prod2 (M,N) iff ( the carrier of b3 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b3 ex x1, y1 being Point of M ex x2, y2 being Point of N st ( x = [x1,x2] & y = [y1,y2] & the distance of b3 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) ); registration let M, N be non empty MetrStruct ; cluster max-Prod2 (M,N) -> non empty strict ; coherence not max-Prod2 (M,N) is empty proof the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1; hence not the carrier of (max-Prod2 (M,N)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition let M, N be non empty MetrStruct ; let x be Point of M; let y be Point of N; :: original: [ redefine func[x,y] -> Element of (max-Prod2 (M,N)); coherence [x,y] is Element of (max-Prod2 (M,N)) proof [x,y] is Element of (max-Prod2 (M,N)) by Def1; hence [x,y] is Element of (max-Prod2 (M,N)) ; ::_thesis: verum end; end; definition let M, N be non empty MetrStruct ; let x be Point of (max-Prod2 (M,N)); :: original: `1 redefine funcx `1 -> Element of M; coherence x `1 is Element of M proof the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1; hence x `1 is Element of M by MCART_1:10; ::_thesis: verum end; :: original: `2 redefine funcx `2 -> Element of N; coherence x `2 is Element of N proof the carrier of (max-Prod2 (M,N)) = [: the carrier of M, the carrier of N:] by Def1; hence x `2 is Element of N by MCART_1:10; ::_thesis: verum end; end; theorem Th18: :: TOPREAL7:18 for M, N being non empty MetrStruct for m1, m2 being Point of M for 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 ; ::_thesis: for m1, m2 being Point of M for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2))) let m1, m2 be Point of M; ::_thesis: for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2))) let n1, n2 be Point of N; ::_thesis: dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2))) consider x1, y1 being Point of M, x2, y2 being Point of N such that A1: [m1,n1] = [x1,x2] and A2: [m2,n2] = [y1,y2] and A3: the distance of (max-Prod2 (M,N)) . ([m1,n1],[m2,n2]) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; A4: m2 = y1 by A2, XTUPLE_0:1; ( m1 = x1 & n1 = x2 ) by A1, XTUPLE_0:1; hence dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2))) by A2, A3, A4, XTUPLE_0:1; ::_thesis: verum end; theorem :: TOPREAL7:19 for M, N being non empty MetrStruct for 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 ; ::_thesis: for m, n being Point of (max-Prod2 (M,N)) holds dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) let m, n be Point of (max-Prod2 (M,N)); ::_thesis: dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) consider x1, y1 being Point of M, x2, y2 being Point of N such that A1: m = [x1,x2] and A2: n = [y1,y2] and A3: the distance of (max-Prod2 (M,N)) . (m,n) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; A4: m `2 = x2 by A1, MCART_1:7; ( m `1 = x1 & n `1 = y1 ) by A1, A2, MCART_1:7; hence dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) by A2, A3, A4, MCART_1:7; ::_thesis: verum end; theorem Th20: :: TOPREAL7:20 for M, N being non empty Reflexive MetrStruct holds max-Prod2 (M,N) is Reflexive proof let M, N be non empty Reflexive MetrStruct ; ::_thesis: max-Prod2 (M,N) is Reflexive let a be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_2,METRIC_1:def_6 ::_thesis: the distance of (max-Prod2 (M,N)) . (a,a) = 0 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; the distance of M is Reflexive by METRIC_1:def_6; then A3: the distance of M . (x1,x1) = 0 by METRIC_1:def_2; the distance of N is Reflexive by METRIC_1:def_6; then A4: the distance of N . (x2,x2) = 0 by METRIC_1:def_2; ( x1 = y1 & x2 = y2 ) by A1, XTUPLE_0:1; hence the distance of (max-Prod2 (M,N)) . (a,a) = 0 by A2, A3, A4; ::_thesis: verum end; registration let M, N be non empty Reflexive MetrStruct ; cluster max-Prod2 (M,N) -> strict Reflexive ; coherence max-Prod2 (M,N) is Reflexive by Th20; end; Lm1: for M, N being non empty MetrSpace holds max-Prod2 (M,N) is discerning proof let M, N be non empty MetrSpace; ::_thesis: max-Prod2 (M,N) is discerning let a, b be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_3,METRIC_1:def_7 ::_thesis: ( not the distance of (max-Prod2 (M,N)) . (a,b) = 0 or a = b ) assume A1: the distance of (max-Prod2 (M,N)) . (a,b) = 0 ; ::_thesis: a = b A2: the distance of M is discerning by METRIC_1:def_7; consider x1, y1 being Point of M, x2, y2 being Point of N such that A3: ( a = [x1,x2] & b = [y1,y2] ) and A4: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; 0 <= dist (x1,y1) by METRIC_1:5; then the distance of M . (x1,y1) = 0 by A1, A4, XXREAL_0:49; then A5: ( the distance of N is discerning & x1 = y1 ) by A2, METRIC_1:def_3, METRIC_1:def_7; 0 <= dist (x2,y2) by METRIC_1:5; then the distance of N . (x2,y2) = 0 by A1, A4, XXREAL_0:49; hence a = b by A3, A5, METRIC_1:def_3; ::_thesis: verum end; theorem Th21: :: TOPREAL7:21 for M, N being non empty symmetric MetrStruct holds max-Prod2 (M,N) is symmetric proof let M, N be non empty symmetric MetrStruct ; ::_thesis: max-Prod2 (M,N) is symmetric let a, b be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_4,METRIC_1:def_8 ::_thesis: the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a) consider x1, y1 being Point of M, x2, y2 being Point of N such that A1: a = [x1,x2] and A2: b = [y1,y2] and A3: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; consider m1, n1 being Point of M, m2, n2 being Point of N such that A4: b = [m1,m2] and A5: a = [n1,n2] and A6: the distance of (max-Prod2 (M,N)) . (b,a) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1; A7: x1 = n1 by A1, A5, XTUPLE_0:1; the distance of N is symmetric by METRIC_1:def_8; then A8: the distance of N . (x2,y2) = the distance of N . (y2,x2) by METRIC_1:def_4; the distance of M is symmetric by METRIC_1:def_8; then A9: the distance of M . (x1,y1) = the distance of M . (y1,x1) by METRIC_1:def_4; ( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1; hence the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a) by A1, A3, A5, A6, A9, A8, A7, XTUPLE_0:1; ::_thesis: verum end; registration let M, N be non empty symmetric MetrStruct ; cluster max-Prod2 (M,N) -> strict symmetric ; coherence max-Prod2 (M,N) is symmetric by Th21; end; theorem Th22: :: TOPREAL7:22 for M, N being non empty triangle MetrStruct holds max-Prod2 (M,N) is triangle proof let M, N be non empty triangle MetrStruct ; ::_thesis: max-Prod2 (M,N) is triangle let a, b, c be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def_5,METRIC_1:def_9 ::_thesis: 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)) consider x1, y1 being Point of M, x2, y2 being Point of N such that A1: a = [x1,x2] and A2: b = [y1,y2] and A3: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; consider m1, n1 being Point of M, m2, n2 being Point of N such that A4: b = [m1,m2] and A5: c = [n1,n2] and A6: the distance of (max-Prod2 (M,N)) . (b,c) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1; A7: ( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1; consider p1, q1 being Point of M, p2, q2 being Point of N such that A8: a = [p1,p2] and A9: c = [q1,q2] and A10: the distance of (max-Prod2 (M,N)) . (a,c) = max (( the distance of M . (p1,q1)),( the distance of N . (p2,q2))) by Def1; A11: ( q1 = n1 & q2 = n2 ) by A5, A9, XTUPLE_0:1; the distance of N is triangle by METRIC_1:def_9; then A12: the distance of N . (p2,q2) <= ( the distance of N . (p2,y2)) + ( the distance of N . (y2,q2)) by METRIC_1:def_5; the distance of M is triangle by METRIC_1:def_9; then A13: the distance of M . (p1,q1) <= ( the distance of M . (p1,y1)) + ( the distance of M . (y1,q1)) by METRIC_1:def_5; ( x1 = p1 & x2 = p2 ) by A1, A8, XTUPLE_0:1; 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 A3, A6, A10, A13, A12, A7, A11, Th2; ::_thesis: verum end; registration let M, N be non empty triangle MetrStruct ; cluster max-Prod2 (M,N) -> strict triangle ; coherence max-Prod2 (M,N) is triangle by Th22; end; registration let M, N be non empty MetrSpace; cluster max-Prod2 (M,N) -> strict discerning ; coherence max-Prod2 (M,N) is discerning by Lm1; end; theorem Th23: :: TOPREAL7:23 for M, N being non empty MetrSpace holds [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N)) proof let M, N be non empty MetrSpace; ::_thesis: [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N)) set S = TopSpaceMetr M; set T = TopSpaceMetr N; A1: TopSpaceMetr (max-Prod2 (M,N)) = TopStruct(# the carrier of (max-Prod2 (M,N)),(Family_open_set (max-Prod2 (M,N))) #) by PCOMPS_1:def_5; A2: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; A3: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5; A4: the carrier of [:(TopSpaceMetr M),(TopSpaceMetr N):] = [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr N):] by BORSUK_1:def_2 .= the carrier of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A2, A3, Def1 ; A5: the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = { (union A) where A is Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] : A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } } by BORSUK_1:def_2; the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = the topology of (TopSpaceMetr (max-Prod2 (M,N))) proof thus the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] c= the topology of (TopSpaceMetr (max-Prod2 (M,N))) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (TopSpaceMetr (max-Prod2 (M,N))) c= the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] or X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) ) assume A6: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] ; ::_thesis: X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) then consider A being Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] such that A7: X = union A and A8: A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A5; for x being Point of (max-Prod2 (M,N)) st x in X holds ex r being Real st ( r > 0 & Ball (x,r) c= X ) proof let x be Point of (max-Prod2 (M,N)); ::_thesis: ( x in X implies ex r being Real st ( r > 0 & Ball (x,r) c= X ) ) assume x in X ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= 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 (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } by A8, A10; then consider X1 being Subset of (TopSpaceMetr M), X2 being Subset of (TopSpaceMetr N) such that A11: Z = [:X1,X2:] and A12: X1 in the topology of (TopSpaceMetr M) and A13: X2 in the topology of (TopSpaceMetr N) ; 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 z2 = z2 as Point of N by A3, A15; consider r2 being Real such that A17: r2 > 0 and A18: Ball (z2,r2) c= X2 by A3, A13, A15, PCOMPS_1:def_4; reconsider z1 = z1 as Point of M by A2, A14; consider r1 being Real such that A19: r1 > 0 and A20: Ball (z1,r1) c= X1 by A2, A12, A14, PCOMPS_1:def_4; take r = min (r1,r2); ::_thesis: ( r > 0 & Ball (x,r) c= X ) thus r > 0 by A19, A17, XXREAL_0:15; ::_thesis: Ball (x,r) c= X let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (x,r) or b in X ) assume A21: b in Ball (x,r) ; ::_thesis: b in X then reconsider bb = b as Point of (max-Prod2 (M,N)) ; A22: dist (bb,x) < r by A21, METRIC_1:11; consider x1, y1 being Point of M, x2, y2 being Point of N such that A23: bb = [x1,x2] and A24: x = [y1,y2] and A25: the distance of (max-Prod2 (M,N)) . (bb,x) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1; z2 = y2 by A16, A24, XTUPLE_0:1; then the distance of N . (x2,z2) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25; then ( min (r1,r2) <= r2 & the distance of N . (x2,z2) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17; then dist (x2,z2) < r2 by XXREAL_0:2; then A26: x2 in Ball (z2,r2) by METRIC_1:11; z1 = y1 by A16, A24, XTUPLE_0:1; then the distance of M . (x1,z1) <= max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by XXREAL_0:25; then ( min (r1,r2) <= r1 & the distance of M . (x1,z1) < r ) by A25, A22, XXREAL_0:2, XXREAL_0:17; then dist (x1,z1) < r1 by XXREAL_0:2; then x1 in Ball (z1,r1) by METRIC_1:11; then b in [:X1,X2:] by A20, A18, A23, A26, ZFMISC_1:87; hence b in X by A7, A10, A11, TARSKI:def_4; ::_thesis: verum end; hence X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) by A1, A4, A6, PCOMPS_1:def_4; ::_thesis: verum end; let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) or X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] ) assume A27: X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) ; ::_thesis: X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] then reconsider Y = X as Subset of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A4; A28: Base-Appr Y = { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( [:X1,Y1:] c= Y & X1 is open & Y1 is open ) } by BORSUK_1:def_3; A29: union (Base-Appr Y) = Y proof thus union (Base-Appr Y) c= Y by BORSUK_1:12; :: according to XBOOLE_0:def_10 ::_thesis: Y c= union (Base-Appr Y) let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Y or u in union (Base-Appr Y) ) assume A30: u in Y ; ::_thesis: u in union (Base-Appr Y) then reconsider uu = u as Point of (max-Prod2 (M,N)) by A1, A4; consider r being Real such that A31: r > 0 and A32: Ball (uu,r) c= Y by A1, A27, A30, PCOMPS_1:def_4; uu in the carrier of (max-Prod2 (M,N)) ; then uu in [: the carrier of M, the carrier of N:] by Def1; then consider u1, u2 being set such that A33: u1 in the carrier of M and A34: u2 in the carrier of N and A35: u = [u1,u2] by ZFMISC_1:def_2; reconsider u2 = u2 as Point of N by A34; reconsider u1 = u1 as Point of M by A33; reconsider B2 = Ball (u2,r) as Subset of (TopSpaceMetr N) by A3; reconsider B1 = Ball (u1,r) as Subset of (TopSpaceMetr M) by A2; ( u1 in Ball (u1,r) & u2 in Ball (u2,r) ) by A31, TBSP_1:11; then A36: u in [:B1,B2:] by A35, ZFMISC_1:87; A37: [:B1,B2:] c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:B1,B2:] or x in Y ) assume x in [:B1,B2:] ; ::_thesis: x in Y then consider x1, x2 being set such that A38: x1 in B1 and A39: x2 in B2 and A40: x = [x1,x2] by ZFMISC_1:def_2; reconsider x2 = x2 as Point of N by A39; reconsider x1 = x1 as Point of M by A38; consider p1, p2 being Point of M, q1, q2 being Point of N such that A41: ( uu = [p1,q1] & [x1,x2] = [p2,q2] ) and A42: the distance of (max-Prod2 (M,N)) . (uu,[x1,x2]) = max (( the distance of M . (p1,p2)),( the distance of N . (q1,q2))) by Def1; ( u2 = q1 & x2 = q2 ) by A35, A41, XTUPLE_0:1; then A43: dist (q1,q2) < r by A39, METRIC_1:11; ( u1 = p1 & x1 = p2 ) by A35, A41, XTUPLE_0:1; then dist (p1,p2) < r by A38, METRIC_1:11; then dist (uu,[x1,x2]) < r by A42, A43, XXREAL_0:16; then x in Ball (uu,r) by A40, METRIC_1:11; hence x in Y by A32; ::_thesis: verum end; ( B1 is open & B2 is open ) by TOPMETR:14; then [:B1,B2:] in Base-Appr Y by A28, A37; hence u in union (Base-Appr Y) by A36, TARSKI:def_4; ::_thesis: verum end; Base-Appr Y c= { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Base-Appr Y or A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } ) assume A in Base-Appr Y ; ::_thesis: A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } then consider X1 being Subset of (TopSpaceMetr M), Y1 being Subset of (TopSpaceMetr N) such that A44: A = [:X1,Y1:] and [:X1,Y1:] c= Y and A45: ( X1 is open & Y1 is open ) by A28; ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) by A45, PRE_TOPC:def_2; hence A in { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) } by A44; ::_thesis: verum end; hence X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] by A5, A29; ::_thesis: verum end; hence [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N)) by A4; ::_thesis: verum end; theorem :: TOPREAL7:24 for M, N being non empty MetrSpace st the carrier of M = the carrier of N & ( for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) holds TopSpaceMetr M = TopSpaceMetr N proof let M, N be non empty MetrSpace; ::_thesis: ( the carrier of M = the carrier of N & ( for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) implies TopSpaceMetr M = TopSpaceMetr N ) assume that A1: the carrier of M = the carrier of N and A2: for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) and A3: for m being Point of M for n being Point of N for r being Real st r > 0 & m = n holds ex r1 being Real st ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ; ::_thesis: TopSpaceMetr M = TopSpaceMetr N A4: Family_open_set M = Family_open_set N proof thus Family_open_set M c= Family_open_set N :: according to XBOOLE_0:def_10 ::_thesis: Family_open_set N c= Family_open_set M proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Family_open_set M or X in Family_open_set N ) assume A5: X in Family_open_set M ; ::_thesis: X in Family_open_set N for n being Point of N st n in X holds ex r being Real st ( r > 0 & Ball (n,r) c= X ) proof let n be Point of N; ::_thesis: ( n in X implies ex r being Real st ( r > 0 & Ball (n,r) c= X ) ) assume A6: n in X ; ::_thesis: ex r being Real st ( r > 0 & Ball (n,r) c= 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_4; consider r1 being Real such that A9: ( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) by A2, A7; take r1 ; ::_thesis: ( r1 > 0 & Ball (n,r1) c= X ) thus ( r1 > 0 & Ball (n,r1) c= X ) by A8, A9, XBOOLE_1:1; ::_thesis: verum end; hence X in Family_open_set N by A1, A5, PCOMPS_1:def_4; ::_thesis: verum end; let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Family_open_set N or X in Family_open_set M ) assume A10: X in Family_open_set N ; ::_thesis: X in Family_open_set M for m being Point of M st m in X holds ex r being Real st ( r > 0 & Ball (m,r) c= X ) proof let m be Point of M; ::_thesis: ( m in X implies ex r being Real st ( r > 0 & Ball (m,r) c= X ) ) assume A11: m in X ; ::_thesis: ex r being Real st ( r > 0 & Ball (m,r) c= 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_4; consider r1 being Real such that A14: ( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) by A3, A12; take r1 ; ::_thesis: ( r1 > 0 & Ball (m,r1) c= X ) thus ( r1 > 0 & Ball (m,r1) c= X ) by A13, A14, XBOOLE_1:1; ::_thesis: verum end; hence X in Family_open_set M by A1, A10, PCOMPS_1:def_4; ::_thesis: verum end; TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; hence TopSpaceMetr M = TopSpaceMetr N by A1, A4, PCOMPS_1:def_5; ::_thesis: verum end; Lm2: for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) proof let i, j be Element of NAT ; ::_thesis: ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) set ci = the carrier of (Euclid i); set cj = the carrier of (Euclid j); set cij = the carrier of (Euclid (i + j)); defpred S1[ Element of the carrier of (Euclid i), Element of the carrier of (Euclid j), set ] means ex fi, fj being FinSequence of REAL st ( fi = \$1 & fj = \$2 & \$3 = fi ^ fj ); A1: the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12; A2: for x being Element of the carrier of (Euclid i) for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u] proof let x be Element of the carrier of (Euclid i); ::_thesis: for y being Element of the carrier of (Euclid j) ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u] let y be Element of the carrier of (Euclid j); ::_thesis: ex u being Element of the carrier of (Euclid (i + j)) st S1[x,y,u] ( x is Element of REAL i & y is Element of REAL j ) ; then reconsider fi = x, fj = y as FinSequence of REAL ; fi ^ fj is Tuple of i + j, REAL by FINSEQ_2:107; then reconsider u = fi ^ fj as Element of the carrier of (Euclid (i + j)) by FINSEQ_2:131; take u ; ::_thesis: S1[x,y,u] thus S1[x,y,u] ; ::_thesis: verum end; consider f being Function of [: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)) such that A3: for x being Element of the carrier of (Euclid i) for y being Element of the carrier of (Euclid j) holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A2); A4: [: the carrier of (Euclid i), the carrier of (Euclid j):] = the carrier of (max-Prod2 ((Euclid i),(Euclid j))) by Def1; the carrier of (TopSpaceMetr (Euclid (i + j))) = the carrier of (Euclid (i + j)) by TOPMETR:12; then reconsider f = f as Function of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))),(TopSpaceMetr (Euclid (i + j))) by A4, A1; A5: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] = TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j))) by Th23; then reconsider f = f as Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) ; take f ; ::_thesis: ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) thus dom f = [#] [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] (TopSpaceMetr (Euclid (i + j))) & f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) thus A6: rng f = [#] (TopSpaceMetr (Euclid (i + j))) ::_thesis: ( f is one-to-one & f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) proof thus rng f c= [#] (TopSpaceMetr (Euclid (i + j))) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (TopSpaceMetr (Euclid (i + j))) c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] (TopSpaceMetr (Euclid (i + j))) or y in rng f ) assume y in [#] (TopSpaceMetr (Euclid (i + j))) ; ::_thesis: y in rng f then reconsider k = y as Element of REAL (i + j) by TOPMETR:12; len k = i + j by CARD_1:def_7; then consider g, h being FinSequence of REAL such that A7: ( len g = i & len h = j ) and A8: k = g ^ h by FINSEQ_2:23; A9: ( g in the carrier of (Euclid i) & h in the carrier of (Euclid j) ) by A7, Th16; then [g,h] in [: the carrier of (Euclid i), the carrier of (Euclid j):] by ZFMISC_1:87; then A10: [g,h] in dom f by FUNCT_2:def_1; ex fi, fj being FinSequence of REAL st ( fi = g & fj = h & f . (g,h) = fi ^ fj ) by A3, A9; hence y in rng f by A8, A10, FUNCT_1:def_3; ::_thesis: verum end; thus A11: f is one-to-one ::_thesis: ( f is continuous & f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume x1 in dom f ; ::_thesis: ( not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) then consider x1a, x1b being set such that A12: x1a in the carrier of (Euclid i) and A13: x1b in the carrier of (Euclid j) and A14: x1 = [x1a,x1b] by A4, A1, A5, ZFMISC_1:def_2; assume x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) then consider x2a, x2b being set such that A15: x2a in the carrier of (Euclid i) and A16: x2b in the carrier of (Euclid j) and A17: x2 = [x2a,x2b] by A4, A1, A5, ZFMISC_1:def_2; assume A18: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider fi1, fj1 being FinSequence of REAL such that A19: fi1 = x1a and A20: fj1 = x1b and A21: f . (x1a,x1b) = fi1 ^ fj1 by A3, A12, A13; consider fi2, fj2 being FinSequence of REAL such that A22: fi2 = x2a and A23: fj2 = x2b and A24: f . (x2a,x2b) = fi2 ^ fj2 by A3, A15, A16; len fj1 = j by A13, A20, CARD_1:def_7; then A25: len fj1 = len fj2 by A16, A23, CARD_1:def_7; A26: len fi1 = i by A12, A19, CARD_1:def_7; then len fi1 = len fi2 by A15, A22, CARD_1:def_7; then fi1 = fi2 by A14, A17, A21, A24, A25, A18, Th5; hence x1 = x2 by A14, A17, A19, A20, A21, A22, A23, A24, A26, A25, A18, Th5; ::_thesis: verum end; A27: 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)))); ::_thesis: ( P is open implies (f ") " P is open ) assume P is open ; ::_thesis: (f ") " P is open then P in the topology of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) by PRE_TOPC:def_2; then A28: P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by TOPMETR:12; A29: for x being Point of (Euclid (i + j)) st x in f .: P holds ex r being Real st ( r > 0 & Ball (x,r) c= f .: P ) proof let x be Point of (Euclid (i + j)); ::_thesis: ( x in f .: P implies ex r being Real st ( r > 0 & Ball (x,r) c= f .: P ) ) assume x in f .: P ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= f .: P ) then consider a being set such that A30: a in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) and A31: a in P and A32: x = f . a by FUNCT_2:64; reconsider a = a as Point of (max-Prod2 ((Euclid i),(Euclid j))) by A30, TOPMETR:12; consider r being Real such that A33: r > 0 and A34: Ball (a,r) c= P by A28, A31, PCOMPS_1:def_4; take r ; ::_thesis: ( r > 0 & Ball (x,r) c= f .: P ) thus r > 0 by A33; ::_thesis: Ball (x,r) c= f .: P let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (x,r) or b in f .: P ) assume A35: b in Ball (x,r) ; ::_thesis: b in f .: P then reconsider bb = b as Point of (Euclid (i + j)) ; reconsider bb2 = bb, xx2 = x as Element of REAL (i + j) ; dist (bb,x) < r by A35, METRIC_1:11; then |.(bb2 - xx2).| < r by EUCLID:def_6; then A36: sqrt (Sum (sqr (abs (bb2 - xx2)))) < r by EUCLID:25; reconsider k = bb as Element of REAL (i + j) ; len k = i + j by CARD_1:def_7; then consider g, h being FinSequence of REAL such that A37: len g = i and A38: len h = j and A39: k = g ^ h by FINSEQ_2:23; reconsider hh = h as Point of (Euclid j) by A38, Th16; reconsider gg = g as Point of (Euclid i) by A37, Th16; consider g, h being FinSequence of REAL such that A40: g = gg and A41: h = hh and A42: f . (gg,hh) = g ^ h by A3; reconsider gg2 = gg, a12 = a `1 as Element of REAL i ; A43: ( max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (gg,(a `1)) or max ((dist (gg,(a `1))),(dist (hh,(a `2)))) = dist (hh,(a `2)) ) by XXREAL_0:16; consider p, q being set such that A44: p in the carrier of (Euclid i) and A45: q in the carrier of (Euclid j) and A46: a = [p,q] by A4, ZFMISC_1:def_2; reconsider q = q as Element of the carrier of (Euclid j) by A45; reconsider p = p as Element of the carrier of (Euclid i) by A44; consider fi, fj being FinSequence of REAL such that A47: fi = p and A48: fj = q and A49: f . (p,q) = fi ^ fj by A3; A50: ( len fi = i & len fj = j ) by A47, A48, CARD_1:def_7; ( len g = i & len h = j ) by A40, A41, CARD_1:def_7; then sqrt (Sum (sqr ((abs (g - fi)) ^ (abs (h - fj))))) < r by A32, A39, A46, A49, A40, A41, A50, A36, Th15; then sqrt (Sum ((sqr (abs (g - fi))) ^ (sqr (abs (h - fj))))) < r by Th10; then A51: sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) < r by RVSUM_1:75; reconsider hh2 = hh, a22 = a `2 as Element of REAL j ; A52: a22 = q by A46, MCART_1:7; 0 <= Sum (sqr (abs (g - fi))) by RVSUM_1:86; then ( 0 <= Sum (sqr (abs (hh2 - a22))) & (Sum (sqr (abs (hh2 - a22)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A48, A41, A52, RVSUM_1:86, XREAL_1:7; then sqrt (Sum (sqr (abs (hh2 - a22)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26; then sqrt (Sum (sqr (abs (hh2 - a22)))) < r by A51, XXREAL_0:2; then |.(hh2 - a22).| < r by EUCLID:25; then A53: (Pitag_dist j) . (hh2,a22) < r by EUCLID:def_6; A54: a12 = p by A46, MCART_1:7; 0 <= Sum (sqr (abs (h - fj))) by RVSUM_1:86; then ( 0 <= Sum (sqr (abs (gg2 - a12))) & (Sum (sqr (abs (gg2 - a12)))) + 0 <= (Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj)))) ) by A47, A40, A54, RVSUM_1:86, XREAL_1:7; then sqrt (Sum (sqr (abs (gg2 - a12)))) <= sqrt ((Sum (sqr (abs (g - fi)))) + (Sum (sqr (abs (h - fj))))) by SQUARE_1:26; then sqrt (Sum (sqr (abs (gg2 - a12)))) < r by A51, XXREAL_0:2; then |.(gg2 - a12).| < r by EUCLID:25; then A55: (Pitag_dist i) . (gg2,a12) < r by EUCLID:def_6; dist ([gg,hh],[(a `1),(a `2)]) = max ((dist (gg,(a `1))),(dist (hh,(a `2)))) by Th18; then dist ([gg,hh],a) < r by A4, A55, A53, A43, MCART_1:21; then [g,h] in Ball (a,r) by A40, A41, METRIC_1:11; then [g,h] in P by A34; hence b in f .: P by A39, A40, A41, A42, FUNCT_2:35; ::_thesis: verum end; f .: P is Subset of (Euclid (i + j)) by TOPMETR:12; then f .: P in Family_open_set (Euclid (i + j)) by A29, PCOMPS_1:def_4; then f .: P in the topology of (TopSpaceMetr (Euclid (i + j))) by TOPMETR:12; hence (f ") " P in the topology of (TopSpaceMetr (Euclid (i + j))) by A6, A11, A5, TOPS_2:54; :: according to PRE_TOPC:def_2 ::_thesis: verum end; A56: 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))); ::_thesis: ( P is open implies f " P is open ) assume P is open ; ::_thesis: f " P is open then P in the topology of (TopSpaceMetr (Euclid (i + j))) by PRE_TOPC:def_2; then A57: P in Family_open_set (Euclid (i + j)) by TOPMETR:12; A58: for x being Point of (max-Prod2 ((Euclid i),(Euclid j))) st x in f " P holds 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))); ::_thesis: ( x in f " P implies ex r being Real st ( r > 0 & Ball (x,r) c= f " P ) ) assume A59: x in f " P ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= f " P ) then f . x in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5; then reconsider fx = f . x as Point of (Euclid (i + j)) by TOPMETR:12; f . x in P by A59, FUNCT_2:38; then consider r being Real such that A60: r > 0 and A61: Ball (fx,r) c= P by A57, PCOMPS_1:def_4; take r1 = r / 2; ::_thesis: ( r1 > 0 & Ball (x,r1) c= f " P ) thus r1 > 0 by A60, XREAL_1:139; ::_thesis: Ball (x,r1) c= f " P let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (x,r1) or b in f " P ) assume A62: b in Ball (x,r1) ; ::_thesis: b in f " P then reconsider bb = b as Point of (max-Prod2 ((Euclid i),(Euclid j))) ; A63: dist (bb,x) < r1 by A62, METRIC_1:11; bb in the carrier of (max-Prod2 ((Euclid i),(Euclid j))) ; then A64: bb in the carrier of (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) by TOPMETR:12; then f . bb in the carrier of (TopSpaceMetr (Euclid (i + j))) by FUNCT_2:5; then reconsider fb = f . b as Point of (Euclid (i + j)) by TOPMETR:12; reconsider fbb = fb, fxx = fx as Element of REAL (i + j) ; consider b1, x1 being Point of (Euclid i), b2, x2 being Point of (Euclid j) such that A65: ( bb = [b1,b2] & x = [x1,x2] ) and the distance of (max-Prod2 ((Euclid i),(Euclid j))) . (bb,x) = max (( the distance of (Euclid i) . (b1,x1)),( the distance of (Euclid j) . (b2,x2))) by Def1; A66: dist ([b1,b2],[x1,x2]) = max ((dist (b1,x1)),(dist (b2,x2))) by Th18; dist (b2,x2) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25; then A67: dist (b2,x2) < r1 by A65, A66, A63, XXREAL_0:2; reconsider x2i = x2, b2i = b2 as Element of REAL j ; reconsider b1i = b1, x1i = x1 as Element of REAL i ; consider b1f, b2f being FinSequence of REAL such that A68: ( b1f = b1 & b2f = b2 ) and A69: f . (b1,b2) = b1f ^ b2f by A3; A70: ( len b1f = i & len b2f = j ) by A68, CARD_1:def_7; dist (b1,x1) <= max ((dist (b1,x1)),(dist (b2,x2))) by XXREAL_0:25; then dist (b1,x1) < r1 by A65, A66, A63, XXREAL_0:2; then A71: ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) < r1 + r1 by A67, XREAL_1:8; ( 0 <= Sum (sqr (b1i - x1i)) & 0 <= Sum (sqr (b2i - x2i)) ) by RVSUM_1:86; then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= |.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i)))) by SQUARE_1:59; then sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).| by EUCLID:def_6; then A72: sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) <= ((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) by EUCLID:def_6; consider x1f, x2f being FinSequence of REAL such that A73: ( x1f = x1 & x2f = x2 ) and A74: f . (x1,x2) = x1f ^ x2f by A3; A75: ( len x1f = i & len x2f = j ) by A73, CARD_1:def_7; (Pitag_dist (i + j)) . (fbb,fxx) = |.(fbb - fxx).| by EUCLID:def_6 .= sqrt (Sum (sqr (abs (fbb - fxx)))) by EUCLID:25 .= sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i))))) by A65, A68, A69, A73, A74, A70, A75, Th15 .= sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i))))) by Th10 .= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i))))) by RVSUM_1:75 .= sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25 .= sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) by EUCLID:25 ; then dist (fb,fx) < r by A72, A71, XXREAL_0:2; then f . b in Ball (fx,r) by METRIC_1:11; hence b in f " P by A61, A64, FUNCT_2:38; ::_thesis: verum end; f " P is Subset of (max-Prod2 ((Euclid i),(Euclid j))) by A5, TOPMETR:12; then f " P in Family_open_set (max-Prod2 ((Euclid i),(Euclid j))) by A58, PCOMPS_1:def_4; hence f " P in the topology of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] by A5, TOPMETR:12; :: according to PRE_TOPC:def_2 ::_thesis: verum end; [#] (TopSpaceMetr (Euclid (i + j))) <> {} ; hence f is continuous by A56, TOPS_2:43; ::_thesis: ( f " is continuous & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) [#] (TopSpaceMetr (max-Prod2 ((Euclid i),(Euclid j)))) <> {} ; hence f " is continuous by A27, A5, TOPS_2:43; ::_thesis: for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj let fi, fj be FinSequence; ::_thesis: ( [fi,fj] in dom f implies f . (fi,fj) = fi ^ fj ) assume A76: [fi,fj] in dom f ; ::_thesis: f . (fi,fj) = fi ^ fj then reconsider Fi = fi as Element of the carrier of (Euclid i) by A1, A5, A4, ZFMISC_1:87; reconsider Fj = fj as Element of the carrier of (Euclid j) by A76, A1, A5, A4, ZFMISC_1:87; S1[Fi,Fj,f . (Fi,Fj)] by A3; hence f . (fi,fj) = fi ^ fj ; ::_thesis: verum end; theorem :: TOPREAL7:25 for i, j being Element of NAT holds [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic proof let i, j be Element of NAT ; ::_thesis: [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic consider f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) such that A1: f is being_homeomorphism and for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj by Lm2; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus f is being_homeomorphism by A1; ::_thesis: verum end; theorem :: TOPREAL7:26 for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st ( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds f . (fi,fj) = fi ^ fj ) ) by Lm2;