:: REALSET2 semantic presentation begin definitionfunc :::"add_2"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Num 2) equals :: REALSET2:def 1 (Set (Set "(" (Set "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )); func :::"mult_2"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Num 2) equals :: REALSET2:def 2 (Set (Set "(" (Set "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"add_2"::: REALSET2:def 1 : (Bool (Set ($#k1_realset2 :::"add_2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))); :: deftheorem defines :::"mult_2"::: REALSET2:def 2 : (Bool (Set ($#k2_realset2 :::"mult_2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k13_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Num 1) "," (Num 1) ")" ($#k13_funcop_1 :::".-->"::: ) (Num 1) ")" ))); definitionfunc :::"dL-Z_2"::: -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: REALSET2:def 3 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Num 2) "," (Set ($#k1_realset2 :::"add_2"::: ) ) "," (Set ($#k2_realset2 :::"mult_2"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ")" ")" ) "#)" ); end; :: deftheorem defines :::"dL-Z_2"::: REALSET2:def 3 : (Bool (Set ($#k3_realset2 :::"dL-Z_2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Num 2) "," (Set ($#k1_realset2 :::"add_2"::: ) ) "," (Set ($#k2_realset2 :::"mult_2"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ")" ")" ) "#)" )); registration cluster (Set ($#k3_realset2 :::"dL-Z_2"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster (Set ($#k3_realset2 :::"dL-Z_2"::: ) ) -> ($#v3_rlvect_1 :::"add-associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_realset2 :::"dL-Z_2"::: ) )) -> ($#v6_membered :::"natural-membered"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_realset2 :::"dL-Z_2"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_realset2 :::"dL-Z_2"::: ) )); end; definitionlet "L" be ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; attr "L" is :::"Field-like"::: means :: REALSET2:def 4 (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "L") "is" ($#m3_realset1 :::"DnT"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool "(" "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) "L")) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) (Set "(" ($#k8_struct_0 :::"NonZero"::: ) "L" ")" )))) "holds" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set (Var "B")) "," (Set (Var "P")) "," (Set (Var "e")) "#)" ) "is" ($#l2_algstr_0 :::"AbGroup":::)))) ")" ) ")" ); end; :: deftheorem defines :::"Field-like"::: REALSET2:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_realset2 :::"Field-like"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "L"))) "is" ($#m3_realset1 :::"DnT"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool "(" "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "L")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "L")) ")" )))) "holds" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set (Var "B")) "," (Set (Var "P")) "," (Set (Var "e")) "#)" ) "is" ($#l2_algstr_0 :::"AbGroup":::)))) ")" ) ")" ) ")" )); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "od" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "nd" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "om" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "nm" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); cluster (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" "A" "," "od" "," "om" "," "nm" "," "nd" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v1_realset2 :::"Field-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionlet "F" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"omf"::: "F" -> ($#m3_realset1 :::"DnT"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") equals :: REALSET2:def 5 (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "F"); end; :: deftheorem defines :::"omf"::: REALSET2:def 5 : (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k4_realset2 :::"omf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F"))))); theorem :: REALSET2:1 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "F"))) "#)" ) "is" ($#l2_algstr_0 :::"AbGroup":::))) ; theorem :: REALSET2:2 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: REALSET2:3 (Bool "for" (Set (Var "F")) "being" ($#l2_algstr_0 :::"AbGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )))) ; theorem :: REALSET2:4 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))))) ; theorem :: REALSET2:5 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))))) ; theorem :: REALSET2:6 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: REALSET2:7 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) (Bool "ex" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F")))) ")" )))) ; theorem :: REALSET2:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))))) ; theorem :: REALSET2:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: REALSET2:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "F"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F")))) & (Bool (Set (Set "(" ($#k4_realset2 :::"omf"::: ) (Set (Var "F")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F")))) & (Bool (Set (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F")))) ")" ))) ; theorem :: REALSET2:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ))))) ; theorem :: REALSET2:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ))))) ; theorem :: REALSET2:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))))) ; theorem :: REALSET2:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))))) ; theorem :: REALSET2:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ))))) ; theorem :: REALSET2:16 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) ; theorem :: REALSET2:17 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) ; theorem :: REALSET2:18 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "holds" (Bool (Set (Set "(" ($#k4_realset2 :::"omf"::: ) (Set (Var "F")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F")))))) ; theorem :: REALSET2:19 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))))) ; theorem :: REALSET2:20 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))))) ; theorem :: REALSET2:21 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "F")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"revf"::: "F" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) "F" ")" ) means :: REALSET2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) "F") "holds" (Bool (Set (Set "(" ($#k4_realset2 :::"omf"::: ) "F" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "F"))); end; :: deftheorem defines :::"revf"::: REALSET2:def 6 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_realset2 :::"revf"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool (Set (Set "(" ($#k4_realset2 :::"omf"::: ) (Set (Var "F")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F"))))) ")" ))); theorem :: REALSET2:22 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "st" (Bool (Bool (Set (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_realset2 :::"revf"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))))) ; theorem :: REALSET2:23 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_realset2 :::"revf"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k5_realset2 :::"revf"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: REALSET2:24 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_realset2 :::"omf"::: ) (Set (Var "F")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F")))) & (Bool (Set (Set "(" ($#k5_realset2 :::"revf"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F")))) ")" ))) ; theorem :: REALSET2:25 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: REALSET2:26 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "F"))) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "st" (Bool (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))))) ; registration cluster ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_realset2 :::"Field-like"::: ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end;