:: TOPREAL7 semantic presentation begin theorem :: TOPREAL7:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k7_real_1 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" )))) ; theorem :: TOPREAL7:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b")) ($#k7_real_1 :::"+"::: ) (Set (Var "c")))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "e")) ($#k7_real_1 :::"+"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_square_1 :::"max"::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "b")) "," (Set (Var "e")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "c")) "," (Set (Var "f")) ")" ")" )))) ; theorem :: TOPREAL7:3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g")) ")" )))) ; theorem :: TOPREAL7:4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "i")) ($#k5_real_1 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))))) ; theorem :: TOPREAL7:5 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "k")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "k")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "k"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )) ; theorem :: TOPREAL7:6 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) "or" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ; theorem :: TOPREAL7:7 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) "or" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ; theorem :: TOPREAL7:8 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: TOPREAL7:9 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: TOPREAL7:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "g")) ")" )))) ; theorem :: TOPREAL7:11 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "f")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "g")) ")" )))) ; theorem :: TOPREAL7:12 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "k")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "f")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "g")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" )))) ; theorem :: TOPREAL7:13 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "k")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k3_euclid :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "g")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" )))) ; theorem :: TOPREAL7:14 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "k")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "g")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "k")) ")" ) ")" )))) ; theorem :: TOPREAL7:15 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "k")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k3_euclid :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "g")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "k")) ")" ) ")" )))) ; theorem :: TOPREAL7:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREAL7:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; definitionlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"max-Prod2"::: "(" "M" "," "N" ")" -> ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) means :: TOPREAL7:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" it (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" "M"(Bool "ex" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" "N" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" it) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" "M") ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" "N") ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" )) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"max-Prod2"::: TOPREAL7:def 1 : (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "b3")) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))(Bool "ex" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "b3"))) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "M"))) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "N"))) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" )) ")" ))) ")" ) ")" ) ")" ))); registrationlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ; end; definitionlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "N")); :: original: :::"["::: redefine func :::"[":::"x" "," "y":::"]"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ")" ); end; definitionlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Const "M")) "," (Set (Const "N")) ")" ")" ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"Element":::) "of" "M"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"Element":::) "of" "N"; end; theorem :: TOPREAL7:18 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set ($#k2_topreal7 :::"["::: ) (Set (Var "m1")) "," (Set (Var "n1")) ($#k2_topreal7 :::"]"::: ) ) "," (Set ($#k2_topreal7 :::"["::: ) (Set (Var "m2")) "," (Set (Var "n2")) ($#k2_topreal7 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "m1")) "," (Set (Var "m2")) ")" ")" ) "," (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" ) ")" ))))) ; theorem :: TOPREAL7:19 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ")" ) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "m")) ($#k3_topreal7 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "n")) ($#k3_topreal7 :::"`1"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "m")) ($#k4_topreal7 :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "n")) ($#k4_topreal7 :::"`2"::: ) ")" ) ")" ")" ) ")" )))) ; theorem :: TOPREAL7:20 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ) "is" ($#v6_metric_1 :::"Reflexive"::: ) )) ; registrationlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v6_metric_1 :::"Reflexive"::: ) ; end; theorem :: TOPREAL7:21 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ) "is" ($#v8_metric_1 :::"symmetric"::: ) )) ; registrationlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v8_metric_1 :::"symmetric"::: ) ; end; theorem :: TOPREAL7:22 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ) "is" ($#v9_metric_1 :::"triangle"::: ) )) ; registrationlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v9_metric_1 :::"triangle"::: ) ; end; registrationlet "M", "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster (Set ($#k1_topreal7 :::"max-Prod2"::: ) "(" "M" "," "N" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v7_metric_1 :::"discerning"::: ) ; end; theorem :: TOPREAL7:23 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k1_topreal7 :::"max-Prod2"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ")" )))) ; theorem :: TOPREAL7:24 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "n")) "," (Set (Var "r1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "m")) "," (Set (Var "r")) ")" )) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "m")) "," (Set (Var "r1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "n")) "," (Set (Var "r")) ")" )) ")" )))) ")" )) "holds" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N"))))) ; theorem :: TOPREAL7:25 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "i")) ")" ) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "j")) ")" ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ")" )) ($#r1_t_0topsp :::"are_homeomorphic"::: ) )) ; theorem :: TOPREAL7:26 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "i")) ")" ) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "j")) ")" ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool "(" "for" (Set (Var "fi")) "," (Set (Var "fj")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "fi")) "," (Set (Var "fj")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "fi")) "," (Set (Var "fj")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "fi")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "fj")))) ")" ) ")" ))) ;