:: ALGSTR_4 semantic presentation begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "n") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; end; definitionlet "X", "x" be ($#m1_hidden :::"set"::: ) ; func :::"IFXFinSequence"::: "(" "x" "," "X" ")" -> ($#m1_hidden :::"XFinSequence":::) "of" equals :: ALGSTR_4:def 1 "x" if (Bool "x" "is" ($#m1_hidden :::"XFinSequence":::) "of" ) otherwise (Set ($#k4_afinsq_1 :::"<%>"::: ) "X"); end; :: deftheorem defines :::"IFXFinSequence"::: ALGSTR_4:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) "is" ($#m1_hidden :::"XFinSequence":::) "of" )) "implies" (Bool (Set ($#k1_algstr_4 :::"IFXFinSequence"::: ) "(" (Set (Var "x")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "x")) "is" (Bool "not" ($#m1_hidden :::"XFinSequence":::) "of" ))) "implies" (Bool (Set ($#k1_algstr_4 :::"IFXFinSequence"::: ) "(" (Set (Var "x")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_afinsq_1 :::"<%>"::: ) (Set (Var "X")))) ")" ")" )); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "X")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "," (Set (Const "X")); let "c" be ($#m1_hidden :::"XFinSequence":::) "of" ; :: original: :::"."::: redefine func "f" :::"."::: "c" -> ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; theorem :: ALGSTR_4:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set (Var "X")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set (Var "X"))))) ; scheme :: ALGSTR_4:sch 1 FuncRecursiveUniq{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"Function":::), F3() -> ($#m1_hidden :::"Function":::) } : (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) provided (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F2 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" (Set F2 "(" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" ) and (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" (Set F3 "(" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" ) proof end; scheme :: ALGSTR_4:sch 2 FuncRecursiveExist{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )) proof end; scheme :: ALGSTR_4:sch 3 FuncRecursiveUniqu2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"XFinSequence":::) "of" ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_relset_1 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" (Set F3 "(" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ))) and (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" (Set F4 "(" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ))) proof end; scheme :: ALGSTR_4:sch 4 FuncRecursiveExist2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"XFinSequence":::) "of" ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "n")) ")" ) ")" )))) proof end; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); pred "f" :::"extends"::: "g" means :: ALGSTR_4:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "g") ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "f" ($#r1_partfun1 :::"tolerates"::: ) "g") ")" ); end; :: deftheorem defines :::"extends"::: ALGSTR_4:def 2 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_algstr_4 :::"extends"::: ) (Set (Var "g"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) ")" ) ")" )); registration cluster ($#v2_struct_0 :::"empty"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; begin definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); attr "R" is :::"compatible"::: means :: ALGSTR_4:def 3 (Bool "for" (Set (Var "v")) "," (Set (Var "v9")) "," (Set (Var "w")) "," (Set (Var "w9")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set (Var "v9")) ")" )) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set (Var "w9")) ")" ))) "holds" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set "(" (Set (Var "v9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w9")) ")" ) ")" ))); end; :: deftheorem defines :::"compatible"::: ALGSTR_4:def 3 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_algstr_4 :::"compatible"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "v9")) "," (Set (Var "w")) "," (Set (Var "w9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "v9")) ")" )) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w9")) ")" ))) "holds" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "v9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w9")) ")" ) ")" ))) ")" ))); registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k1_eqrel_1 :::"nabla"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) -> ($#v1_algstr_4 :::"compatible"::: ) ; end; registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) bbbadV3_RELAT_2() bbbadV8_RELAT_2() ($#v1_algstr_4 :::"compatible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: ALGSTR_4:2 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_algstr_4 :::"compatible"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "v9")) "," (Set (Var "w")) "," (Set (Var "w9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "v9")) ")" )) & (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w9")) ")" ))) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "v9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w9")) ")" ) ")" ))) ")" ))) ; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); func :::"ClassOp"::: "R" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "R" ")" ) means :: ALGSTR_4:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "R") (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set (Var "v")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set (Var "w")) ")" ))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set "(" (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w")) ")" ) ")" )))) if (Bool (Bool "not" "M" "is" ($#v2_struct_0 :::"empty"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"ClassOp"::: ALGSTR_4:def 4 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "M")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_algstr_4 :::"ClassOp"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R"))) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "v")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w")) ")" ))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w")) ")" ) ")" )))) ")" ) ")" & "(" (Bool (Bool (Set (Var "M")) "is" ($#v2_struct_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_algstr_4 :::"ClassOp"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )))); definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); func "M" :::"./."::: "R" -> ($#l3_algstr_0 :::"multMagma"::: ) equals :: ALGSTR_4:def 5 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "R" ")" ) "," (Set "(" ($#k3_algstr_4 :::"ClassOp"::: ) "R" ")" ) "#)" ); end; :: deftheorem defines :::"./."::: ALGSTR_4:def 5 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "M")) ($#k4_algstr_4 :::"./."::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k3_algstr_4 :::"ClassOp"::: ) (Set (Var "R")) ")" ) "#)" )))); registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); cluster (Set "M" ($#k4_algstr_4 :::"./."::: ) "R") -> ($#v15_algstr_0 :::"strict"::: ) ; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); cluster (Set "M" ($#k4_algstr_4 :::"./."::: ) "R") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); func :::"nat_hom"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" "M" "," (Set "(" "M" ($#k4_algstr_4 :::"./."::: ) "R" ")" ) means :: ALGSTR_4:def 6 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set (Var "v")) ")" ))); end; :: deftheorem defines :::"nat_hom"::: ALGSTR_4:def 6 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set "(" (Set (Var "M")) ($#k4_algstr_4 :::"./."::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_algstr_4 :::"nat_hom"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "v")) ")" ))) ")" )))); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); cluster (Set ($#k5_algstr_4 :::"nat_hom"::: ) "R") -> ($#v1_group_6 :::"multiplicative"::: ) ; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "M")); cluster (Set ($#k5_algstr_4 :::"nat_hom"::: ) "R") -> ($#v2_funct_2 :::"onto"::: ) ; end; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; mode Relators of "M" is (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "r" be ($#m1_hidden :::"Relators":::) "of" (Set (Const "M")); func :::"equ_rel"::: "r" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "M" equals :: ALGSTR_4:def 7 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "R")) where R "is" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "M" : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "r")) & (Bool (Set "r" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w")) ")" )))) "}" ); end; :: deftheorem defines :::"equ_rel"::: ALGSTR_4:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"Relators":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_algstr_4 :::"equ_rel"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "R")) where R "is" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "r")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w")) ")" )))) "}" )))); theorem :: ALGSTR_4:3 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"Relators":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "r")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set (Var "w")) ")" ))) ")" )) "holds" (Bool (Set ($#k6_algstr_4 :::"equ_rel"::: ) (Set (Var "r"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "R")))))) ; registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "r" be ($#m1_hidden :::"Relators":::) "of" (Set (Const "M")); cluster (Set ($#k6_algstr_4 :::"equ_rel"::: ) "r") -> ($#v1_algstr_4 :::"compatible"::: ) ; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"equ_kernel"::: "f" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: ALGSTR_4:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )); end; :: deftheorem defines :::"equ_kernel"::: ALGSTR_4:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_algstr_4 :::"equ_kernel"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )))); theorem :: ALGSTR_4:4 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool (Set ($#k7_algstr_4 :::"equ_kernel"::: ) (Set (Var "f"))) "is" ($#v1_algstr_4 :::"compatible"::: ) ))) ; theorem :: ALGSTR_4:5 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Relators":::) "of" (Set (Var "M")) "st" (Bool (Set ($#k7_algstr_4 :::"equ_kernel"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_algstr_4 :::"equ_rel"::: ) (Set (Var "r"))))))) ; begin definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; mode :::"multSubmagma"::: "of" "M" -> ($#l3_algstr_0 :::"multMagma"::: ) means :: ALGSTR_4:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "M") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"multSubmagma"::: ALGSTR_4:def 9 : (Bool "for" (Set (Var "M")) "," (Set (Var "b2")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" )); registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v15_algstr_0 :::"strict"::: ) for ($#m1_algstr_4 :::"multSubmagma"::: ) "of" "M"; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m1_algstr_4 :::"multSubmagma"::: ) "of" "M"; end; theorem :: ALGSTR_4:6 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "N")) "," (Set (Var "K")) "being" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "K"))) & (Bool (Set (Var "K")) "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "N")))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) "#)" )))) ; theorem :: ALGSTR_4:7 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) "#)" )))) ; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); attr "A" is :::"stable"::: means :: ALGSTR_4:def 10 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r2_hidden :::"in"::: ) "A")); end; :: deftheorem defines :::"stable"::: ALGSTR_4:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_algstr_4 :::"stable"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))); registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v2_algstr_4 :::"stable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); end; theorem :: ALGSTR_4:8 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))))) ; registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "N" be ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Const "M")); cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") -> ($#v2_algstr_4 :::"stable"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "M"; end; theorem :: ALGSTR_4:9 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))) ")" )) "holds" (Bool (Set ($#k4_funct_6 :::"meet"::: ) (Set (Var "F"))) "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))))) ; theorem :: ALGSTR_4:10 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_algstr_4 :::"stable"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))) ; theorem :: ALGSTR_4:11 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) (Bool "for" (Set (Var "X")) "being" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")))))) ; theorem :: ALGSTR_4:12 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) (Bool "for" (Set (Var "Y")) "being" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")))))) ; theorem :: ALGSTR_4:13 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) : (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")))) "}" "is" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))))) ; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "A" be ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); func :::"the_mult_induced_by"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" "A" equals :: ALGSTR_4:def 11 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "M") ($#k1_realset1 :::"||"::: ) "A"); end; :: deftheorem defines :::"the_mult_induced_by"::: ALGSTR_4:def 11 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_algstr_4 :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k8_algstr_4 :::"the_mult_induced_by"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) ($#k1_realset1 :::"||"::: ) (Set (Var "A")))))); definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); func :::"the_submagma_generated_by"::: "A" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_algstr_4 :::"multSubmagma"::: ) "of" "M" means :: ALGSTR_4:def 12 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool "(" "for" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_algstr_4 :::"multSubmagma"::: ) "of" "M" "st" (Bool (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "holds" (Bool it "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "N"))) ")" ) ")" ); end; :: deftheorem defines :::"the_submagma_generated_by"::: ALGSTR_4:def 12 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "b3")) "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )))); theorem :: ALGSTR_4:14 (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "iff" (Bool (Set ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set (Var "A"))) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" ))) ; registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); cluster (Set ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) "A") -> ($#v2_struct_0 :::"empty"::: ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: ALGSTR_4:15 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set (Var "X")) ")" ))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" ) ")" )))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"free_magma_seq"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k1_yellow_6 :::"the_universe_of"::: ) (Set "(" "X" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ) ")" ) means :: ALGSTR_4:def 13 (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "fs")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fs"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "fs")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set (Var "fs")) ")" ))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"free_magma_seq"::: ALGSTR_4:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k1_yellow_6 :::"the_universe_of"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_algstr_4 :::"free_magma_seq"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "fs")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fs"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "fs")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set (Var "fs")) ")" ))) ")" )) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); func :::"free_magma"::: "(" "X" "," "n" ")" -> ($#m1_hidden :::"set"::: ) equals :: ALGSTR_4:def 14 (Set (Set "(" ($#k10_algstr_4 :::"free_magma_seq"::: ) "X" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"free_magma"::: ALGSTR_4:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_algstr_4 :::"free_magma_seq"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "n" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ALGSTR_4:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ALGSTR_4:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: ALGSTR_4:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: ALGSTR_4:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Num 3) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: ALGSTR_4:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "fs")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fs"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "fs")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set (Var "fs")) ")" ))) ")" )))) ; theorem :: ALGSTR_4:21 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "p")) ")" )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" )) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )))) ; theorem :: ALGSTR_4:22 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "n")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: ALGSTR_4:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "Y")) "," (Set (Var "n")) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"free_magma_carrier"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: ALGSTR_4:def 15 (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set "(" (Set "(" ($#k10_algstr_4 :::"free_magma_seq"::: ) "X" ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"free_magma_carrier"::: ALGSTR_4:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set "(" (Set "(" ($#k10_algstr_4 :::"free_magma_seq"::: ) (Set (Var "X")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) ")" ) ")" )))); theorem :: ALGSTR_4:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Const "X"))); cluster (Set "w" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v7_ordinal1 :::"natural"::: ) for ($#m1_hidden :::"number"::: ) ; end; theorem :: ALGSTR_4:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) "holds" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: ALGSTR_4:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "v")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X")))))) ; theorem :: ALGSTR_4:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "Y"))))) ; theorem :: ALGSTR_4:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"free_magma_mult"::: "X" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k12_algstr_4 :::"free_magma_carrier"::: ) "X" ")" ) means :: ALGSTR_4:def 16 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) "X") (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) )) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "v")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) )))) if (Bool (Bool "not" "X" "is" ($#v1_xboole_0 :::"empty"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"free_magma_mult"::: ALGSTR_4:def 16 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_algstr_4 :::"free_magma_mult"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) )) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "v")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_algstr_4 :::"free_magma_mult"::: ) (Set (Var "X")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"free_magma"::: "X" -> ($#l3_algstr_0 :::"multMagma"::: ) equals :: ALGSTR_4:def 17 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k12_algstr_4 :::"free_magma_carrier"::: ) "X" ")" ) "," (Set "(" ($#k13_algstr_4 :::"free_magma_mult"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"free_magma"::: ALGSTR_4:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" ($#k12_algstr_4 :::"free_magma_carrier"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k13_algstr_4 :::"free_magma_mult"::: ) (Set (Var "X")) ")" ) "#)" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_algstr_4 :::"free_magma"::: ) "X") -> ($#v15_algstr_0 :::"strict"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_algstr_4 :::"free_magma"::: ) "X") -> ($#v2_struct_0 :::"empty"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_algstr_4 :::"free_magma"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; let "w" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Const "X")) ")" ); cluster (Set "w" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v7_ordinal1 :::"natural"::: ) for ($#m1_hidden :::"number"::: ) ; end; theorem :: ALGSTR_4:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "S"))) "is" ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "w" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Const "X")) ")" ); func :::"length"::: "w" -> ($#m1_hidden :::"Nat":::) equals :: ALGSTR_4:def 18 (Set "w" ($#k2_xtuple_0 :::"`2"::: ) ) if (Bool (Bool "not" "X" "is" ($#v1_xboole_0 :::"empty"::: ) )) otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"length"::: ALGSTR_4:def 18 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" & "(" (Bool (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))); theorem :: ALGSTR_4:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "w")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) : (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Num 1)) "}" )) ; theorem :: ALGSTR_4:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "v")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" ($#k15_algstr_4 :::"length"::: ) (Set (Var "v")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k15_algstr_4 :::"length"::: ) (Set (Var "w")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: ALGSTR_4:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "v")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "v")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ))) ; theorem :: ALGSTR_4:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set "(" (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_algstr_4 :::"length"::: ) (Set (Var "v")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k15_algstr_4 :::"length"::: ) (Set (Var "w")) ")" ))))) ; theorem :: ALGSTR_4:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w"))) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w2")))) & (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w")))) & (Bool (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w2"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k15_algstr_4 :::"length"::: ) (Set (Var "w")))) ")" )))) ; theorem :: ALGSTR_4:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Set (Var "v1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w2"))))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "w2"))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); func :::"canon_image"::: "(" "X" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "n" ")" ")" ) "," (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) "X" ")" ) means :: ALGSTR_4:def 19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," "n" ($#k4_tarski :::"]"::: ) ))) if (Bool "n" ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"canon_image"::: ALGSTR_4:def 19 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ")" ) "," (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "n")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k16_algstr_4 :::"canon_image"::: ) "(" "X" "," "n" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: ALGSTR_4:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set (Var "A")))))) ; theorem :: ALGSTR_4:37 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) ($#k4_algstr_4 :::"./."::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k9_algstr_4 :::"the_submagma_generated_by"::: ) (Set "(" (Set "(" ($#k5_algstr_4 :::"nat_hom"::: ) (Set (Var "R")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" ) ")" ))))) ; theorem :: ALGSTR_4:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "Y")) "," (Num 1) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "Y")) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "n", "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Const "X")) "," (Set (Const "n")) ")" ")" ) "," (Set (Const "M")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Const "X")) "," (Set (Const "m")) ")" ")" ) "," (Set (Const "M")); func :::"[:":::"f" "," "g":::":]"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "n" ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "m" ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "n" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," "M" means :: ALGSTR_4:def 20 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "n" ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "m" ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "n" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "n" ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" "X" "," "m" ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "g" ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" )))))); end; :: deftheorem defines :::"[:"::: ALGSTR_4:def 20 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "M")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "M")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k17_algstr_4 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k17_algstr_4 :::":]"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ")" ) "," (Set "(" ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "n")) ")" ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_algstr_4 :::"free_magma"::: ) "(" (Set (Var "X")) "," (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Set (Var "b7")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" )))))) ")" ))))))); theorem :: ALGSTR_4:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "M")) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "," (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set (Var "h")) ($#r1_algstr_4 :::"extends"::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ))) ")" ))))) ; theorem :: ALGSTR_4:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "M")) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "," (Set (Var "M")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set (Var "h")) ($#r1_algstr_4 :::"extends"::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ))) & (Bool (Set (Var "g")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set (Var "g")) ($#r1_algstr_4 :::"extends"::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" )))) "holds" (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Var "g"))))))) ; theorem :: ALGSTR_4:41 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_algstr_4 :::"multSubmagma"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set ($#k7_algstr_4 :::"equ_kernel"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "M")) ($#k4_algstr_4 :::"./."::: ) (Set (Var "R")) ")" ) "," (Set (Var "H")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_algstr_4 :::"nat_hom"::: ) (Set (Var "R")) ")" ))) & (Bool (Set (Var "g")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) ")" )))))) ; theorem :: ALGSTR_4:42 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R")) "being" ($#v1_algstr_4 :::"compatible"::: ) ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "M")) ($#k4_algstr_4 :::"./."::: ) (Set (Var "R")) ")" ) "," (Set (Var "N")) "st" (Bool (Bool (Set (Set (Var "g1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_algstr_4 :::"nat_hom"::: ) (Set (Var "R")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g2")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_algstr_4 :::"nat_hom"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set (Var "g1")) ($#r2_relset_1 :::"="::: ) (Set (Var "g2")))))) ; theorem :: ALGSTR_4:43 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Relators":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" )(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) ($#k4_algstr_4 :::"./."::: ) (Set "(" ($#k6_algstr_4 :::"equ_rel"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) ")" ))))) ; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"free_magmaF"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) "X" ")" ) "," (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) "Y" ")" ) means :: ALGSTR_4:def 21 (Bool "(" (Bool it "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool it ($#r1_algstr_4 :::"extends"::: ) (Set (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" "Y" "," (Num 1) ")" ")" ) ($#k1_partfun1 :::"*"::: ) "f" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" "X" "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ))) ")" ); end; :: deftheorem defines :::"free_magmaF"::: ALGSTR_4:def 21 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_algstr_4 :::"free_magma"::: ) (Set (Var "Y")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "b4")) "is" ($#v1_group_6 :::"multiplicative"::: ) ) & (Bool (Set (Var "b4")) ($#r1_algstr_4 :::"extends"::: ) (Set (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "Y")) "," (Num 1) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_algstr_4 :::"canon_image"::: ) "(" (Set (Var "X")) "," (Num 1) ")" ")" ) ($#k2_funct_1 :::"""::: ) ")" ))) ")" ) ")" )))); registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k18_algstr_4 :::"free_magmaF"::: ) "f") -> ($#v1_group_6 :::"multiplicative"::: ) ; end; theorem :: ALGSTR_4:44 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "g")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f")) ")" )))))) ; theorem :: ALGSTR_4:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f"))) ($#r1_funct_2 :::"="::: ) (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "g"))))))) ; theorem :: ALGSTR_4:46 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f")) ")" ) ")" ))))) ; theorem :: ALGSTR_4:47 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: ALGSTR_4:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set ($#k18_algstr_4 :::"free_magmaF"::: ) (Set (Var "f"))) "is" ($#v2_funct_2 :::"onto"::: ) ))) ;