:: VALUED_0 semantic presentation begin definitionlet "f" be ($#m1_hidden :::"Relation":::); attr "f" is :::"complex-valued"::: means :: VALUED_0:def 1 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); attr "f" is :::"ext-real-valued"::: means :: VALUED_0:def 2 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )); attr "f" is :::"real-valued"::: means :: VALUED_0:def 3 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )); canceled; canceled; attr "f" is :::"natural-valued"::: means :: VALUED_0:def 6 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"complex-valued"::: VALUED_0:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )); :: deftheorem defines :::"ext-real-valued"::: VALUED_0:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" )); :: deftheorem defines :::"real-valued"::: VALUED_0:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_valued_0 :::"real-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" )); :: deftheorem VALUED_0:def 4 : canceled; :: deftheorem VALUED_0:def 5 : canceled; :: deftheorem defines :::"natural-valued"::: VALUED_0:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v6_membered :::"natural-membered"::: ) ; end; theorem :: VALUED_0:1 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ))) ; theorem :: VALUED_0:2 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ))) ; theorem :: VALUED_0:3 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" ($#v3_valued_0 :::"real-valued"::: ) ))) ; theorem :: VALUED_0:4 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ))) ; theorem :: VALUED_0:5 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ))) ; theorem :: VALUED_0:6 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "S")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "R")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ))) ; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> ($#v2_valued_0 :::"ext-real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); cluster -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "R"); end; registrationlet "R", "S" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "R", "S" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "R", "S" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "R", "S" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R", "S" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R", "S" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_xboole_0 :::"\/"::: ) "S") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> ($#v1_valued_0 :::"complex-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> ($#v3_valued_0 :::"real-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); let "S" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_xboole_0 :::"/\"::: ) "S") -> ($#v4_valued_0 :::"natural-valued"::: ) ; cluster (Set "R" ($#k4_xboole_0 :::"\"::: ) "S") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "R", "S" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "R", "S" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "R", "S" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "R", "S" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R", "S" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R", "S" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_xboole_0 :::"\+\"::: ) "S") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v1_membered :::"complex-membered"::: ) ; end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v2_membered :::"ext-real-membered"::: ) ; end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v3_membered :::"real-membered"::: ) ; end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v4_membered :::"rational-membered"::: ) ; end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_relat_1 :::"Im"::: ) "(" "R" "," "x" ")" ) -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "R" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "R" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "R" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "R" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "X" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "S" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_relat_1 :::"*"::: ) "S") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is :::"complex-valued"::: means :: VALUED_0:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xcmplx_0 :::"complex"::: ) )); redefine attr "f" is :::"ext-real-valued"::: means :: VALUED_0:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xxreal_0 :::"ext-real"::: ) )); redefine attr "f" is :::"real-valued"::: means :: VALUED_0:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xreal_0 :::"real"::: ) )); canceled; canceled; redefine attr "f" is :::"natural-valued"::: means :: VALUED_0:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_ordinal1 :::"natural"::: ) )); end; :: deftheorem defines :::"complex-valued"::: VALUED_0:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xcmplx_0 :::"complex"::: ) )) ")" )); :: deftheorem defines :::"ext-real-valued"::: VALUED_0:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xxreal_0 :::"ext-real"::: ) )) ")" )); :: deftheorem defines :::"real-valued"::: VALUED_0:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_valued_0 :::"real-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xreal_0 :::"real"::: ) )) ")" )); :: deftheorem VALUED_0:def 10 : canceled; :: deftheorem VALUED_0:def 11 : canceled; :: deftheorem defines :::"natural-valued"::: VALUED_0:def 12 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_ordinal1 :::"natural"::: ) )) ")" )); theorem :: VALUED_0:7 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xcmplx_0 :::"complex"::: ) )) ")" )) ; theorem :: VALUED_0:8 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xxreal_0 :::"ext-real"::: ) )) ")" )) ; theorem :: VALUED_0:9 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_valued_0 :::"real-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_xreal_0 :::"real"::: ) )) ")" )) ; theorem :: VALUED_0:10 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_rat_1 :::"rational"::: ) )) ")" )) ; theorem :: VALUED_0:11 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_int_1 :::"integer"::: ) )) ")" )) ; theorem :: VALUED_0:12 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_ordinal1 :::"natural"::: ) )) ")" )) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_xcmplx_0 :::"complex"::: ) ; end; registrationlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_xxreal_0 :::"ext-real"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_rat_1 :::"rational"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_int_1 :::"integer"::: ) ; end; registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v7_ordinal1 :::"natural"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "f", "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f", "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "f", "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f", "g" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f", "g" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f", "g" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#m1_hidden :::"Nat":::); cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_valued_0 :::"ext-real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; notationlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Relation":::); synonym :::"non-zero"::: "f" for :::"non-empty"::: ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: VALUED_0:13 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_funct_1 :::"constant"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: VALUED_0:14 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_funct_1 :::"constant"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: VALUED_0:15 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_funct_1 :::"constant"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: VALUED_0:16 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v3_funct_1 :::"constant"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: VALUED_0:17 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v3_funct_1 :::"constant"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: VALUED_0:18 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_funct_1 :::"constant"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; begin definitionlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); attr "f" is :::"increasing"::: means :: VALUED_0:def 13 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e2")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))); attr "f" is :::"decreasing"::: means :: VALUED_0:def 14 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e2")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::">"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))); attr "f" is :::"non-decreasing"::: means :: VALUED_0:def 15 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e2")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))); attr "f" is :::"non-increasing"::: means :: VALUED_0:def 16 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e2")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::">="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))); end; :: deftheorem defines :::"increasing"::: VALUED_0:def 13 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e2")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))) ")" )); :: deftheorem defines :::"decreasing"::: VALUED_0:def 14 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e2")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))) ")" )); :: deftheorem defines :::"non-decreasing"::: VALUED_0:def 15 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e2")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))) ")" )); :: deftheorem defines :::"non-increasing"::: VALUED_0:def 16 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "e1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e2")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))))) ")" )); registration cluster ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) ($#v6_valued_0 :::"decreasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v6_valued_0 :::"decreasing"::: ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v8_valued_0 :::"non-increasing"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f", "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v5_valued_0 :::"increasing"::: ) ; end; registrationlet "f", "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v7_valued_0 :::"non-decreasing"::: ) ; end; registrationlet "f", "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v6_valued_0 :::"decreasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v5_valued_0 :::"increasing"::: ) ; end; registrationlet "f", "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v8_valued_0 :::"non-increasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v7_valued_0 :::"non-decreasing"::: ) ; end; registrationlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v6_valued_0 :::"decreasing"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v6_valued_0 :::"decreasing"::: ) ; cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v6_valued_0 :::"decreasing"::: ) ; end; registrationlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v8_valued_0 :::"non-increasing"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v8_valued_0 :::"non-increasing"::: ) ; cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v8_valued_0 :::"non-increasing"::: ) ; end; registrationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v5_valued_0 :::"increasing"::: ) for ($#m1_subset_1 :::"Function":::) "of" "X" "," "X"; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "s" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"subsequence"::: "of" "s" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: VALUED_0:def 17 (Bool "ex" (Set (Var "N")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool it ($#r1_hidden :::"="::: ) (Set "s" ($#k3_relat_1 :::"*"::: ) (Set (Var "N"))))); end; :: deftheorem defines :::"subsequence"::: VALUED_0:def 17 : (Bool "for" (Set (Var "s")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_valued_0 :::"subsequence"::: ) "of" (Set (Var "s"))) "iff" (Bool "ex" (Set (Var "N")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "N"))))) ")" )); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_valued_0 :::"subsequence"::: ) "of" "s"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"subsequence"::: redefine mode :::"subsequence"::: "of" "s" -> ($#m1_subset_1 :::"sequence":::) "of" "X"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "k" be ($#m1_hidden :::"Nat":::); :: original: :::"^\"::: redefine func "s" :::"^\"::: "k" -> ($#m2_valued_0 :::"subsequence"::: ) "of" "s"; end; theorem :: VALUED_0:19 (Bool "for" (Set (Var "XX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ss")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "XX")) "holds" (Bool (Set (Var "ss")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "ss"))))) ; theorem :: VALUED_0:20 (Bool "for" (Set (Var "XX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ss1")) "," (Set (Var "ss2")) "," (Set (Var "ss3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "XX")) "st" (Bool (Bool (Set (Var "ss1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "ss2"))) & (Bool (Set (Var "ss2")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "ss3")))) "holds" (Bool (Set (Var "ss1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "ss3"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: VALUED_0:21 (Bool "for" (Set (Var "XX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ss")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "XX")) (Bool "for" (Set (Var "ss1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "ss")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "ss1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "ss"))))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster -> ($#v3_funct_1 :::"constant"::: ) for ($#m1_valued_0 :::"subsequence"::: ) "of" "s"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "N" be ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"*"::: redefine func "s" :::"*"::: "N" -> ($#m2_valued_0 :::"subsequence"::: ) "of" "s"; end; theorem :: VALUED_0:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "s1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s")))) "holds" (Bool (Set (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s1"))) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s"))))))) ; registrationlet "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster -> ($#v2_relat_1 :::"non-empty"::: ) for ($#m1_valued_0 :::"subsequence"::: ) "of" "s"; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"constant"::: redefine attr "s" is :::"constant"::: means :: VALUED_0:def 18 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"constant"::: VALUED_0:def 18 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ))); theorem :: VALUED_0:23 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: VALUED_0:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set (Var "s")) "is" bbbadV3_FUNCT_1()))) ; theorem :: VALUED_0:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set (Var "s")) "is" bbbadV3_FUNCT_1()))) ; theorem :: VALUED_0:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Var "s1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s")))) "holds" (Bool (Set (Var "s")) ($#r2_funct_2 :::"="::: ) (Set (Var "s1"))))) ; theorem :: VALUED_0:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "s")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ))))))) ; theorem :: VALUED_0:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))))))) ; theorem :: VALUED_0:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "s")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")))))))) ; theorem :: VALUED_0:30 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s")) ")" )))))) ; theorem :: VALUED_0:31 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "h1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h1")) ")" )))) "holds" (Bool (Set (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "h2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h1")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "s"))))))))) ; definitionlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); attr "f" is :::"zeroed"::: means :: VALUED_0:def 19 (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"zeroed"::: VALUED_0:def 19 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_valued_0 :::"zeroed"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v2_valued_0 :::"ext-real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "s" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); redefine attr "s" is :::"constant"::: means :: VALUED_0:def 20 (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"constant"::: VALUED_0:def 20 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" )); theorem :: VALUED_0:32 (Bool "for" (Set (Var "x")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_valued_0 :::"subsequence"::: ) "of" (Set (Var "M")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "M"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end;