:: AFVECT0 semantic presentation begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"WeakAffVect-like"::: means :: AFVECT0:def 1 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ); end; :: deftheorem defines :::"WeakAffVect-like"::: AFVECT0:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_afvect0 :::"WeakAffVect-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v1_afvect0 :::"WeakAffVect-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode WeakAffVect is ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_afvect0 :::"WeakAffVect-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdgroup :::"AffVect-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_afvect0 :::"WeakAffVect-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: AFVECT0:1 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: AFVECT0:2 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a"))))) ; theorem :: AFVECT0:3 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: AFVECT0:4 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: AFVECT0:5 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d9")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))))) ; theorem :: AFVECT0:6 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b"))))) ; theorem :: AFVECT0:7 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "d")) "," (Set (Var "c"))))) ; theorem :: AFVECT0:8 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) ; theorem :: AFVECT0:9 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "d9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))))) ; theorem :: AFVECT0:10 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "d9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9")))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))))) ; theorem :: AFVECT0:11 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9"))) & (Bool (Set (Var "b")) "," (Set (Var "f")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b9")) "," (Set (Var "f9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "d9")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "f")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "f9"))))) ; theorem :: AFVECT0:12 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "b9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "c9")) "," (Set (Var "a9"))))) ; definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); pred :::"MDist"::: "a" "," "b" means :: AFVECT0:def 2 (Bool "(" (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "b" "," "a") & (Bool "a" ($#r1_hidden :::"<>"::: ) "b") ")" ); irreflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")) "holds" (Bool "(" "not" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "a"))) "or" "not" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" )) ; symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" )) ; end; :: deftheorem defines :::"MDist"::: AFVECT0:def 2 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" ) ")" ))); theorem :: AFVECT0:13 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Bool "not" ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b")))) ")" ))) ; theorem :: AFVECT0:14 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) "holds" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "b")) "," (Set (Var "c"))))) ; theorem :: AFVECT0:15 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "a", "b", "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); pred :::"Mid"::: "a" "," "b" "," "c" means :: AFVECT0:def 3 (Bool "a" "," "b" ($#r2_analoaf :::"//"::: ) "b" "," "c"); end; :: deftheorem defines :::"Mid"::: AFVECT0:def 3 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ))); theorem :: AFVECT0:16 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))))) ; theorem :: AFVECT0:17 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: AFVECT0:18 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" ))) ; theorem :: AFVECT0:19 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))))) ; theorem :: AFVECT0:20 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b9")) "," (Set (Var "c"))) & (Bool (Bool "not" (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) "holds" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "b")) "," (Set (Var "b9"))))) ; theorem :: AFVECT0:21 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))))) ; theorem :: AFVECT0:22 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))))) ; theorem :: AFVECT0:23 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "b")) "," (Set (Var "b9")))) "holds" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b9")) "," (Set (Var "c"))))) ; theorem :: AFVECT0:24 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "b")) "," (Set (Var "b9")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))))) ; theorem :: AFVECT0:25 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "a9"))) & (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "b9")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))))) ; theorem :: AFVECT0:26 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "a9"))) & (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "b9"))) & (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "a9"))))) ; definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); func :::"PSym"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Element":::) "of" "AFV" means :: AFVECT0:def 4 (Bool ($#r2_afvect0 :::"Mid"::: ) "b" "," "a" "," it); end; :: deftheorem defines :::"PSym"::: AFVECT0:def 4 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "b4"))) ")" ))); theorem :: AFVECT0:27 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "p")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "b"))) ")" ))) ; theorem :: AFVECT0:28 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "p"))) ")" ) ")" ))) ; theorem :: AFVECT0:29 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: AFVECT0:30 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: AFVECT0:31 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: AFVECT0:32 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "b")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" )))) ; theorem :: AFVECT0:33 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "b")) ")" ) ($#r2_analoaf :::"//"::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "c")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" )) ")" ))) ; theorem :: AFVECT0:34 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "b")) ")" )) ")" ))) ; theorem :: AFVECT0:35 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool ($#r2_afvect0 :::"Mid"::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "b")) ")" ) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "c")) ")" )) ")" ))) ; theorem :: AFVECT0:36 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) "or" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ) ")" ))) ; theorem :: AFVECT0:37 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "a")) ")" )))) ; theorem :: AFVECT0:38 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ")" ) ")" )) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) "or" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "p")) "," (Set (Var "q"))) "or" (Bool ($#r1_afvect0 :::"MDist"::: ) (Set (Var "q")) "," (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) ")" ) ")" ))) ; theorem :: AFVECT0:39 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "r")) "," (Set (Var "a")) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "r")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ")" ) ")" ")" ) ")" )))) ; theorem :: AFVECT0:40 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "b")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "c")) "," (Set (Var "p")) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ))))) ; theorem :: AFVECT0:41 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "c")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "c")) "," (Set "(" ($#k1_afvect0 :::"PSym"::: ) "(" (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ")" ))))) ; definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o", "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); func :::"Padd"::: "(" "o" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Element":::) "of" "AFV" means :: AFVECT0:def 5 (Bool "o" "," "a" ($#r2_analoaf :::"//"::: ) "b" "," it); end; :: deftheorem defines :::"Padd"::: AFVECT0:def 5 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_afvect0 :::"Padd"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Var "o")) "," (Set (Var "a")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b5"))) ")" ))); notationlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o", "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); synonym :::"Pcom"::: "(" "o" "," "a" ")" for :::"PSym"::: "(" "o" "," "a" ")" ; end; definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); func :::"Padd"::: "o" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AFV") means :: AFVECT0:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "AFV" "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_afvect0 :::"Padd"::: ) "(" "o" "," (Set (Var "a")) "," (Set (Var "b")) ")" ))); end; :: deftheorem defines :::"Padd"::: AFVECT0:def 6 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFV"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_afvect0 :::"Padd"::: ) (Set (Var "o")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_afvect0 :::"Padd"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))) ")" )))); definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); func :::"Pcom"::: "o" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AFV") means :: AFVECT0:def 7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "AFV" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"Pcom"::: ) "(" "o" "," (Set (Var "a")) ")" ))); end; :: deftheorem defines :::"Pcom"::: AFVECT0:def 7 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFV"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_afvect0 :::"Pcom"::: ) (Set (Var "o")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afvect0 :::"Pcom"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" ))) ")" )))); definitionlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); func :::"GroupVect"::: "(" "AFV" "," "o" ")" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) equals :: AFVECT0:def 8 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AFV") "," (Set "(" ($#k3_afvect0 :::"Padd"::: ) "o" ")" ) "," "o" "#)" ); end; :: deftheorem defines :::"GroupVect"::: AFVECT0:def 8 : (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFV"))) "," (Set "(" ($#k3_afvect0 :::"Padd"::: ) (Set (Var "o")) ")" ) "," (Set (Var "o")) "#)" )))); registrationlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); cluster (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" "AFV" "," "o" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ; end; theorem :: AFVECT0:42 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AFV")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_afvect0 :::"Padd"::: ) (Set (Var "o")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "o"))) ")" ))) ; theorem :: AFVECT0:43 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_afvect0 :::"Padd"::: ) (Set (Var "o")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" )))))) ; registrationlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); cluster (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" "AFV" "," "o" ")" ) -> ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: AFVECT0:44 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ) (Bool "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_afvect0 :::"Pcom"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a9")))))))) ; theorem :: AFVECT0:45 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "o"))))) ; theorem :: AFVECT0:46 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"WeakAffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ) "st" (Bool (Set (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; registrationlet "AFV" be ($#l1_analoaf :::"WeakAffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); cluster (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" "AFV" "," "o" ")" ) -> ($#v8_algstr_0 :::"strict"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) ; end; theorem :: AFVECT0:47 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"AffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" )))))) ; registrationlet "AFV" be ($#l1_analoaf :::"AffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); cluster (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" "AFV" "," "o" ")" ) -> ($#v8_algstr_0 :::"strict"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionmode Proper_Uniquely_Two_Divisible_Group is ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::); end; theorem :: AFVECT0:48 (Bool "for" (Set (Var "AFV")) "being" ($#l1_analoaf :::"AffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ) "is" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::)))) ; registrationlet "AFV" be ($#l1_analoaf :::"AffVect":::); let "o" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AFV")); cluster (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" "AFV" "," "o" ")" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ; end; theorem :: AFVECT0:49 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) "holds" (Bool (Set ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG"))) "is" ($#l1_analoaf :::"AffVect":::))) ; registrationlet "ADG" be ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::); cluster (Set ($#k2_tdgroup :::"AV"::: ) "ADG") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v2_tdgroup :::"AffVect-like"::: ) ; end; theorem :: AFVECT0:50 (Bool "for" (Set (Var "AFV")) "being" ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffVect":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AFV")) "holds" (Bool (Set (Var "AFV")) ($#r1_hidden :::"="::: ) (Set ($#k2_tdgroup :::"AV"::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set (Var "AFV")) "," (Set (Var "o")) ")" ")" ))))) ; theorem :: AFVECT0:51 (Bool "for" (Set (Var "AS")) "being" ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffVect":::)) "iff" (Bool "ex" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) "st" (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG"))))) ")" )) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))); pred "f" :::"is_Iso_of"::: "X" "," "Y" means :: AFVECT0:def 9 (Bool "(" (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y")) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool "(" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "Y")) & (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_Iso_of"::: AFVECT0:def 9 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_afvect0 :::"is_Iso_of"::: ) (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) ")" ) ")" ) ")" ))); definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; pred "X" "," "Y" :::"are_Iso"::: means :: AFVECT0:def 10 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "st" (Bool (Set (Var "f")) ($#r3_afvect0 :::"is_Iso_of"::: ) "X" "," "Y")); end; :: deftheorem defines :::"are_Iso"::: AFVECT0:def 10 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r4_afvect0 :::"are_Iso"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "st" (Bool (Set (Var "f")) ($#r3_afvect0 :::"is_Iso_of"::: ) (Set (Var "X")) "," (Set (Var "Y")))) ")" )); theorem :: AFVECT0:52 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o9")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o9")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_afvect0 :::"Padd"::: ) (Set (Var "o")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "ADG")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "," (Set (Var "o")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_afvect0 :::"Pcom"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ))) ")" )))))) ; theorem :: AFVECT0:53 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o9")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: AFVECT0:54 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o9")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "," (Set (Var "o")) ")" ")" ))))))) ; theorem :: AFVECT0:55 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Proper_Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "o9")))) "holds" (Bool (Set (Var "ADG")) "," (Set ($#k5_afvect0 :::"GroupVect"::: ) "(" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "," (Set (Var "o")) ")" ) ($#r4_afvect0 :::"are_Iso"::: ) )))) ;