:: FUNCT_8 semantic presentation begin definitionlet "A" be ($#m1_hidden :::"set"::: ) ; attr "A" is :::"symmetrical"::: means :: FUNCT_8:def 1 (Bool "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "A")); end; :: deftheorem defines :::"symmetrical"::: FUNCT_8:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_funct_8 :::"symmetrical"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" )); registration cluster ($#v1_membered :::"complex-membered"::: ) ($#v1_funct_8 :::"symmetrical"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k2_numbers :::"COMPLEX"::: ) ))); end; registration cluster ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v1_funct_8 :::"symmetrical"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ))); end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"with_symmetrical_domain"::: means :: FUNCT_8:def 2 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "R") "is" ($#v1_funct_8 :::"symmetrical"::: ) ); end; :: deftheorem defines :::"with_symmetrical_domain"::: FUNCT_8:def 2 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) "is" ($#v1_funct_8 :::"symmetrical"::: ) ) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_funct_8 :::"with_symmetrical_domain"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "R") -> ($#v1_funct_8 :::"symmetrical"::: ) ; end; definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"quasi_even"::: means :: FUNCT_8:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"quasi_even"::: FUNCT_8:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_funct_8 :::"quasi_even"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" ))); definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"even"::: means :: FUNCT_8:def 4 (Bool "(" (Bool "F" "is" ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ) & (Bool "F" "is" ($#v3_funct_8 :::"quasi_even"::: ) ) ")" ); end; :: deftheorem defines :::"even"::: FUNCT_8:def 4 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_funct_8 :::"quasi_even"::: ) ) ")" ) ")" ))); registrationlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ($#v3_funct_8 :::"quasi_even"::: ) -> ($#v4_funct_8 :::"even"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v4_funct_8 :::"even"::: ) -> ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ($#v3_funct_8 :::"quasi_even"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); pred "F" :::"is_even_on"::: "A" means :: FUNCT_8:def 5 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k5_relset_1 :::"|"::: ) "A") "is" ($#v4_funct_8 :::"even"::: ) ) ")" ); end; :: deftheorem defines :::"is_even_on"::: FUNCT_8:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k5_relset_1 :::"|"::: ) (Set (Var "A"))) "is" ($#v4_funct_8 :::"even"::: ) ) ")" ) ")" )))); definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"quasi_odd"::: means :: FUNCT_8:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"quasi_odd"::: FUNCT_8:def 6 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_funct_8 :::"quasi_odd"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); definitionlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"odd"::: means :: FUNCT_8:def 7 (Bool "(" (Bool "F" "is" ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ) & (Bool "F" "is" ($#v5_funct_8 :::"quasi_odd"::: ) ) ")" ); end; :: deftheorem defines :::"odd"::: FUNCT_8:def 7 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_funct_8 :::"quasi_odd"::: ) ) ")" ) ")" ))); registrationlet "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ($#v5_funct_8 :::"quasi_odd"::: ) -> ($#v6_funct_8 :::"odd"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v6_funct_8 :::"odd"::: ) -> ($#v2_funct_8 :::"with_symmetrical_domain"::: ) ($#v5_funct_8 :::"quasi_odd"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); pred "F" :::"is_odd_on"::: "A" means :: FUNCT_8:def 8 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k5_relset_1 :::"|"::: ) "A") "is" ($#v6_funct_8 :::"odd"::: ) ) ")" ); end; :: deftheorem defines :::"is_odd_on"::: FUNCT_8:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k5_relset_1 :::"|"::: ) (Set (Var "A"))) "is" ($#v6_funct_8 :::"odd"::: ) ) ")" ) ")" )))); theorem :: FUNCT_8:1 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_8:2 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_8:3 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ")" ))) ; theorem :: FUNCT_8:4 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:5 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) ; theorem :: FUNCT_8:6 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:7 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: FUNCT_8:8 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" )))))) ; theorem :: FUNCT_8:9 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:10 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:11 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:12 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:13 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:14 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_8:15 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_8:16 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:17 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:18 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k37_valued_1 :::"""::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:19 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k37_valued_1 :::"""::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:20 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "F")) ($#k55_valued_1 :::".|"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:21 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "F")) ($#k55_valued_1 :::".|"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:22 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:23 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:24 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:25 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "r")) ($#k9_valued_1 :::"+"::: ) (Set (Var "F"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_8:26 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_8:27 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k41_valued_1 :::"^2"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:28 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k41_valued_1 :::"^2"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:29 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:30 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:31 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:32 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "G")) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_8:33 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) )) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:34 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:35 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:36 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:37 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) )) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "F")) ($#k55_valued_1 :::".|"::: ) ) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:38 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "F")) ($#k55_valued_1 :::".|"::: ) ) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:39 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k41_valued_1 :::"^2"::: ) ) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:40 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k41_valued_1 :::"^2"::: ) ) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:41 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k9_valued_1 :::"+"::: ) (Set (Var "F"))) "is" ($#v4_funct_8 :::"even"::: ) ))) ; theorem :: FUNCT_8:42 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) "is" ($#v4_funct_8 :::"even"::: ) ))) ; theorem :: FUNCT_8:43 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) "is" ($#v6_funct_8 :::"odd"::: ) ))) ; theorem :: FUNCT_8:44 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) "is" ($#v4_funct_8 :::"even"::: ) ))) ; theorem :: FUNCT_8:45 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:46 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:47 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:48 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:49 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:50 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:51 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:52 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:53 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) "is" ($#v4_funct_8 :::"even"::: ) )) ; theorem :: FUNCT_8:54 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; theorem :: FUNCT_8:55 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_funct_8 :::"even"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_funct_8 :::"odd"::: ) ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")) ")" )) "is" ($#v1_funct_8 :::"symmetrical"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k52_valued_1 :::"/""::: ) (Set (Var "G"))) "is" ($#v6_funct_8 :::"odd"::: ) )) ; begin definitionfunc :::"signum"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: FUNCT_8:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_absvalue :::"sgn"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"signum"::: FUNCT_8:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_8 :::"signum"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_absvalue :::"sgn"::: ) (Set (Var "x"))))) ")" )); theorem :: FUNCT_8:56 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_funct_8 :::"signum"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: FUNCT_8:57 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_funct_8 :::"signum"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) ; theorem :: FUNCT_8:58 (Bool (Set (Set ($#k1_funct_8 :::"signum"::: ) ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: FUNCT_8:59 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_funct_8 :::"signum"::: ) ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set ($#k1_funct_8 :::"signum"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))) ; theorem :: FUNCT_8:60 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_funct_8 :::"signum"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:61 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: FUNCT_8:62 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x"))))) ; theorem :: FUNCT_8:63 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ; theorem :: FUNCT_8:64 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_euclid :::"absreal"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:65 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:66 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k19_sin_cos :::"cos"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; registration cluster (Set ($#k16_sin_cos :::"sin"::: ) ) -> ($#v6_funct_8 :::"odd"::: ) ; end; registration cluster (Set ($#k19_sin_cos :::"cos"::: ) ) -> ($#v4_funct_8 :::"even"::: ) ; end; theorem :: FUNCT_8:67 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:68 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; registration cluster (Set ($#k1_sin_cos2 :::"sinh"::: ) ) -> ($#v6_funct_8 :::"odd"::: ) ; end; registration cluster (Set ($#k4_sin_cos2 :::"cosh"::: ) ) -> ($#v4_funct_8 :::"even"::: ) ; end; theorem :: FUNCT_8:69 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k29_sin_cos :::"tan"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:70 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set ($#k29_sin_cos :::"tan"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:71 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set ($#k30_sin_cos :::"cot"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:72 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:73 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k55_valued_1 :::".|"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:74 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k55_valued_1 :::".|"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:75 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k37_valued_1 :::"""::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:76 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k37_valued_1 :::"""::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:77 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set ($#k16_sin_cos :::"sin"::: ) )) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:78 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:79 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k41_valued_1 :::"^2"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:80 (Bool "for" (Set (Var "A")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k41_valued_1 :::"^2"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "A")))) ; theorem :: FUNCT_8:81 (Bool "for" (Set (Var "B")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) )))) "holds" (Bool (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "B")))) ; theorem :: FUNCT_8:82 (Bool "for" (Set (Var "B")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#r1_funct_8 :::"is_even_on"::: ) (Set (Var "B")))) ; theorem :: FUNCT_8:83 (Bool "for" (Set (Var "B")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds" (Bool (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "B")))) ; theorem :: FUNCT_8:84 (Bool "for" (Set (Var "B")) "being" ($#v1_funct_8 :::"symmetrical"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#r2_funct_8 :::"is_odd_on"::: ) (Set (Var "B")))) ;