:: SETWOP_2 semantic presentation begin theorem :: SETWOP_2:1 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "c1")) ($#r1_hidden :::"<>"::: ) (Set (Var "c2")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k3_setwiseo :::"{."::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k3_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c2")) ")" ) ")" )))))) ; theorem :: SETWOP_2:2 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Bool "not" (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "c")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ")" ))))))) ; theorem :: SETWOP_2:3 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "c1")) ($#r1_hidden :::"<>"::: ) (Set (Var "c2"))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"<>"::: ) (Set (Var "c3"))) & (Bool (Set (Var "c2")) ($#r1_hidden :::"<>"::: ) (Set (Var "c3")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k4_setwiseo :::"{."::: ) (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) ($#k4_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c2")) ")" ) ")" ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c3")) ")" ) ")" )))))) ; theorem :: SETWOP_2:4 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "B1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B1")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B2")) "," (Set (Var "f")) ")" ")" ) ")" )))))) ; theorem :: SETWOP_2:5 (Bool "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C9"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C9")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "s")))) ")" ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "A")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" )))))))) ; theorem :: SETWOP_2:6 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "H")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "H")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWOP_2:7 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f9")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f9")) ")" )))))) ; theorem :: SETWOP_2:8 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e")))))))) ; theorem :: SETWOP_2:9 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "," (Set (Var "d4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d4")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d3")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d4")) ")" ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f9")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" ) ")" ))))))) ; theorem :: SETWOP_2:10 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f9")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" ) ")" )))))) ; theorem :: SETWOP_2:11 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r8_binop_1 :::"="::: ) (Set (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f9")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" ) ")" )))))) ; theorem :: SETWOP_2:12 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "e")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "f")) ")" ")" ) ")" ))))))) ; theorem :: SETWOP_2:13 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "e")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d")) ")" ")" ) ")" ))))))) ; theorem :: SETWOP_2:14 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "f")) ")" ")" ) ")" ))))))) ; theorem :: SETWOP_2:15 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d")) ")" ")" ) ")" ))))))) ; theorem :: SETWOP_2:16 (Bool "for" (Set (Var "C")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "H")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: SETWOP_2:17 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWOP_2:18 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWOP_2:19 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); func :::"[#]"::: "(" "p" "," "d" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "D" equals :: SETWOP_2:def 1 (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_funcop_1 :::"-->"::: ) "d" ")" ) ($#k2_finsop_1 :::"+*"::: ) "p"); end; :: deftheorem defines :::"[#]"::: SETWOP_2:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "d")) ")" ) ($#k2_finsop_1 :::"+*"::: ) (Set (Var "p"))))))); theorem :: SETWOP_2:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "implies" (Bool (Set (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))))) "implies" (Bool (Set (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ")" ))))) ; theorem :: SETWOP_2:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: SETWOP_2:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: SETWOP_2:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: SETWOP_2:24 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_setwop_2 :::"[#]"::: ) "(" (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" )))))) ; notationlet "i" be ($#m1_hidden :::"Nat":::); synonym :::"finSeg"::: "i" for :::"Seg"::: "i"; end; definitionlet "i" be ($#m1_hidden :::"Nat":::); :: original: :::"finSeg"::: redefine func :::"finSeg"::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; notationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); synonym "F" :::"$$"::: "p" for "F" :::""**""::: "p"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); assume (Bool "(" (Bool "(" (Bool (Set (Const "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Const "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Const "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) ")" ) ; redefine func "F" :::""**""::: "p" equals :: SETWOP_2:def 2 (Set "F" ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k3_finsop_1 :::"findom"::: ) "p" ")" ) "," (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" "p" "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) "F" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"$$"::: SETWOP_2:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k3_finsop_1 :::"findom"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k1_setwop_2 :::"[#]"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ")" ) ")" ))))); theorem :: SETWOP_2:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: SETWOP_2:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) ")" )))))) ; theorem :: SETWOP_2:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) ")" ))))))) ; theorem :: SETWOP_2:28 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: SETWOP_2:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: SETWOP_2:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: SETWOP_2:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: SETWOP_2:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "," (Set (Var "d4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d4")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d3")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d4")) ")" ")" ) ")" )) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ))))))) ; theorem :: SETWOP_2:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "," (Set (Var "d4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d4")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d3")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d4")) ")" ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )))))))) ; theorem :: SETWOP_2:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )))))) ; theorem :: SETWOP_2:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ))))))) ; theorem :: SETWOP_2:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d1")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d2")) ")" ) ")" ) ")" )))))) ; theorem :: SETWOP_2:37 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r8_binop_1 :::"="::: ) (Set (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "T2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ))))))) ; theorem :: SETWOP_2:38 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: SETWOP_2:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ))))))) ; theorem :: SETWOP_2:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: SETWOP_2:41 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "p")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "G")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ))))))) ;