:: MORPH_01 semantic presentation begin definitionlet "E" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; mode binary-image of "E" is ($#m1_subset_1 :::"Subset":::) "of" "E"; end; definitionlet "E" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A", "B" be ($#m1_subset_1 :::"binary-image":::) "of" (Set (Const "E")); func "A" :::"(-)"::: "B" -> ($#m1_subset_1 :::"binary-image":::) "of" "E" equals :: MORPH_01:def 1 "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"Element":::) "of" "E" : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "E" "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "A")) "}" ; end; :: deftheorem defines :::"(-)"::: MORPH_01:def 1 : (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) : (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "}" ))); notationlet "a" be ($#m1_subset_1 :::"Real":::); let "E" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); synonym "a" :::"*"::: "A" for "a" :::"(.)"::: "A"; end; theorem :: MORPH_01:1 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E")))) ")" ))) ; theorem :: MORPH_01:2 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MORPH_01:3 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ))) ; theorem :: MORPH_01:4 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))))) "holds" (Bool (Set (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MORPH_01:5 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "b")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "}" )))) ; definitionlet "E" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; mode binary-image-family of "E" is ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E"); end; theorem :: MORPH_01:6 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "b")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "}" )))) ; theorem :: MORPH_01:7 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) : (Bool (Set (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k6_mathmorp :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" ))) ; theorem :: MORPH_01:8 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) : (Bool (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k6_mathmorp :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "}" ))) ; theorem :: MORPH_01:9 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k6_rusub_4 :::"(+)"::: ) (Set (Var "B")) ")" ))) ")" ))) ; definitionlet "E" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); :: original: :::"+"::: redefine func "A" :::"(+)"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E"))); commutativity (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")) "holds" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "A"))))) ; end; theorem :: MORPH_01:10 (Bool "for" (Set (Var "E")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "B")) ")" ) ($#k6_rusub_4 :::"+"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_rusub_4 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MORPH_01:11 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B")) ")" ) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set "(" (Set (Var "B")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MORPH_01:12 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "X")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:13 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:14 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" ) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "X")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:15 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:16 (Bool "for" (Set (Var "E")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "A")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "C")))))) ; theorem :: MORPH_01:17 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B")) ")" ))) ")" )))) ; theorem :: MORPH_01:18 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "X")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:19 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" )))))) ; theorem :: MORPH_01:20 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "X")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))))))) ; theorem :: MORPH_01:21 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:22 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "C")))))) ; theorem :: MORPH_01:23 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "C")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "A")))))) ; theorem :: MORPH_01:24 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "B")) ")" ))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B")) ")" ))) ")" )))) ; theorem :: MORPH_01:25 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B")) ")" ) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set "(" (Set (Var "B")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "C")) ")" ))))) ; begin definitionlet "E" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "B" be ($#m1_subset_1 :::"binary-image":::) "of" (Set (Const "E")); func :::"dilation"::: "B" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E") ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E") ")" ) means :: MORPH_01:def 2 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"binary-image":::) "of" "E" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) "B"))); end; :: deftheorem defines :::"dilation"::: MORPH_01:def 2 : (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_morph_01 :::"dilation"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_morph_01 :::"(+)"::: ) (Set (Var "B"))))) ")" )))); definitionlet "E" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "B" be ($#m1_subset_1 :::"binary-image":::) "of" (Set (Const "E")); func :::"erosion"::: "B" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E") ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E") ")" ) means :: MORPH_01:def 3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"binary-image":::) "of" "E" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) "B"))); end; :: deftheorem defines :::"erosion"::: MORPH_01:def 3 : (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_morph_01 :::"erosion"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_morph_01 :::"(-)"::: ) (Set (Var "B"))))) ")" )))); theorem :: MORPH_01:26 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:27 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "B")))))) ; theorem :: MORPH_01:28 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" )))))) ; theorem :: MORPH_01:29 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"binary-image-family":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) : (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))))) ; theorem :: MORPH_01:30 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "B")))))) ; theorem :: MORPH_01:31 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" )))))) ; theorem :: MORPH_01:32 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: MORPH_01:33 (Bool "for" (Set (Var "E")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"binary-image":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")))) & (Bool (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_morph_01 :::"erosion"::: ) (Set "(" (Set "(" ($#k3_morph_01 :::"dilation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")))) ")" ))) ;