:: EXTREAL1  semantic presentation begin  definitionlet "x", "y" be   ($#m1_subset_1 :::"R_eal":::); :: original: :::"*"::: redefine func "x" :::"*"::: "y" ->   ($#m1_subset_1 :::"R_eal":::); end; 
theorem :: EXTREAL1:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_extreal1 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "b")))))) ; 
 definitionlet "x", "y" be   ($#m1_subset_1 :::"R_eal":::); :: original: :::"/"::: redefine func "x" :::"/"::: "y" ->   ($#m1_subset_1 :::"R_eal":::); end; 
theorem :: EXTREAL1:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_extreal1 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k12_binop_2 :::"/"::: )  (Set (Var "b")))))) ; 
 definitionlet "x" be   ($#m1_subset_1 :::"R_eal":::); func :::"|.":::"x":::".|"::: ->   ($#m1_subset_1 :::"R_eal":::) equals :: EXTREAL1:def 1 "x" if (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  "x")  otherwise (Set   ($#k2_supinf_2 :::"-"::: )  "x"); projectivity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool  "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "b2"))))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b1")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b1")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b1"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "b1"))))  ")"   ")" ))
 ; end; 





:: deftheorem    defines :::"|."::: EXTREAL1:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) "implies" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))))) "implies" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "x"))))  ")"   ")" )); 
 
theorem :: EXTREAL1:3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: EXTREAL1:4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "x"))))) ; 
 registrationlet "x" be   ($#m1_subset_1 :::"R_eal":::); 
cluster (Set  ($#k3_extreal1 :::"|."::: ) "x" ($#k3_extreal1 :::".|"::: ) ) ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; 
theorem :: EXTREAL1:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k11_binop_2 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "a")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: EXTREAL1:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k12_binop_2 :::"/"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "a")) ")" )  ($#k2_extreal1 :::"/"::: )  (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "b")) ")" )))) ; 
 begin  definitionlet "F" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); func  :::"Sum"::: "F" ->   ($#m1_subset_1 :::"R_eal":::) means :: EXTREAL1:def 2 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "F" ")" ))) & (Bool (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "F"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" "F"  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"Sum"::: EXTREAL1:def 2 :  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "F")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "(" (Set (Var "F"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ))  ")" ))); 
 
theorem :: EXTREAL1:7 (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k7_numbers :::"ExtREAL"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_2 :::"0."::: )  )) ; 
 
theorem :: EXTREAL1:8 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: EXTREAL1:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "b"))))) ; 
 
theorem :: EXTREAL1:10 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  "st" (Bool (Bool (Bool  "not" (Set   ($#k2_supinf_1 :::"-infty"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F"))))) & (Bool (Bool  "not" (Set   ($#k2_supinf_1 :::"-infty"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "G")))))) "holds"  (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set  "(" (Set (Var "F"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_extreal1 :::"Sum"::: )  (Set (Var "F")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "("  ($#k4_extreal1 :::"Sum"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: EXTREAL1:11 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")) ")" )  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "s")))) & (Bool (Bool  "not" (Set   ($#k2_supinf_1 :::"-infty"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")))))) "holds"  (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "G")))))) ;