:: ENS_1 semantic presentation begin definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Funcs"::: "V" -> ($#m1_hidden :::"set"::: ) equals :: ENS_1:def 1 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" "V" : (Bool verum) "}" ); end; :: deftheorem defines :::"Funcs"::: ENS_1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) : (Bool verum) "}" ))); registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_ens_1 :::"Funcs"::: ) "V") -> ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ENS_1:1 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V")))) "iff" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" )) ")" ))) ; theorem :: ENS_1:2 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V")))))) ; theorem :: ENS_1:3 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Maps"::: "V" -> ($#m1_hidden :::"set"::: ) equals :: ENS_1:def 2 "{" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" "V", f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) "V") : (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" ) "}" ; end; :: deftheorem defines :::"Maps"::: ENS_1:def 2 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V"))) : (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" ) "}" )); registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_ens_1 :::"Maps"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ENS_1:4 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V")))(Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" ))))) ; theorem :: ENS_1:5 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))))))) ; theorem :: ENS_1:6 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "V")) "," (Set (Var "V")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: ENS_1:7 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")))))) ; registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Const "V"))); cluster (Set "m" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Const "V"))); func :::"dom"::: "m" -> ($#m1_subset_1 :::"Element"::: ) "of" "V" equals :: ENS_1:def 3 (Set (Set "(" "m" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func :::"cod"::: "m" -> ($#m1_subset_1 :::"Element"::: ) "of" "V" equals :: ENS_1:def 4 (Set (Set "(" "m" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"dom"::: ENS_1:def 3 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )))); :: deftheorem defines :::"cod"::: ENS_1:def 4 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )))); theorem :: ENS_1:8 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k3_ens_1 :::"dom"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_ens_1 :::"cod"::: ) (Set (Var "m")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: ENS_1:9 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool (Set (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_ens_1 :::"dom"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k4_ens_1 :::"cod"::: ) (Set (Var "m")) ")" )) ")" ))) ; theorem :: ENS_1:10 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" )))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "V")); func :::"id$"::: "A" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") equals :: ENS_1:def 5 (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) "A" "," "A" ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) "A" ")" ) ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"id$"::: ENS_1:def 5 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k5_ens_1 :::"id$"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k1_domain_1 :::"]"::: ) )))); theorem :: ENS_1:11 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_ens_1 :::"id$"::: ) (Set (Var "A")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set "(" ($#k5_ens_1 :::"id$"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set "(" ($#k5_ens_1 :::"id$"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Const "V"))); assume (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set (Const "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set (Const "m2")))) ; func "m2" :::"*"::: "m1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") equals :: ENS_1:def 6 (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k3_ens_1 :::"dom"::: ) "m1" ")" ) "," (Set "(" ($#k4_ens_1 :::"cod"::: ) "m2" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set "(" "m2" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "m1" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"*"::: ENS_1:def 6 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))))) "holds" (Bool (Set (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k3_ens_1 :::"dom"::: ) (Set (Var "m1")) ")" ) "," (Set "(" ($#k4_ens_1 :::"cod"::: ) (Set (Var "m2")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "m2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "m1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))); theorem :: ENS_1:12 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m2")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "m1")) ($#k2_xtuple_0 :::"`2"::: ) ")" ))) & (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set "(" (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m1")))) & (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set "(" (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m2")))) ")" ))) ; theorem :: ENS_1:13 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m2")) "," (Set (Var "m1")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1")))) & (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m2"))))) "holds" (Bool (Set (Set (Var "m3")) ($#k6_ens_1 :::"*"::: ) (Set "(" (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m3")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m2")) ")" ) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")))))) ; theorem :: ENS_1:14 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Set (Var "m")) ($#k6_ens_1 :::"*"::: ) (Set "(" ($#k5_ens_1 :::"id$"::: ) (Set "(" ($#k3_ens_1 :::"dom"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set (Set "(" ($#k5_ens_1 :::"id$"::: ) (Set "(" ($#k4_ens_1 :::"cod"::: ) (Set (Var "m")) ")" ) ")" ) ($#k6_ens_1 :::"*"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "V")); func :::"Maps"::: "(" "A" "," "B" ")" -> ($#m1_hidden :::"set"::: ) equals :: ENS_1:def 7 "{" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) "A" "," "B" ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) "V") : (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) "A" "," "B" ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ens_1 :::"Maps"::: ) "V")) "}" ; end; :: deftheorem defines :::"Maps"::: ENS_1:def 7 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ens_1 :::"Funcs"::: ) (Set (Var "V"))) : (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")))) "}" ))); theorem :: ENS_1:15 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))))) ; theorem :: ENS_1:16 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: ENS_1:17 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")))))) ; theorem :: ENS_1:18 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) : (Bool verum) "}" ))) ; theorem :: ENS_1:19 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" )))) ; theorem :: ENS_1:20 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Const "V"))); attr "m" is :::"surjective"::: means :: ENS_1:def 8 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "m" ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) "m")); end; :: deftheorem defines :::"surjective"::: ENS_1:def 8 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "m")) "is" ($#v1_ens_1 :::"surjective"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "m")) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m")))) ")" ))); begin definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"fDom"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) "," "V" means :: ENS_1:def 9 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m"))))); func :::"fCod"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) "," "V" means :: ENS_1:def 10 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m"))))); func :::"fComp"::: "V" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) means :: ENS_1:def 11 (Bool "(" (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") "st" (Bool (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")))) ")" ) ")" ); end; :: deftheorem defines :::"fDom"::: ENS_1:def 9 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_ens_1 :::"fDom"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m"))))) ")" ))); :: deftheorem defines :::"fCod"::: ENS_1:def 10 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_ens_1 :::"fCod"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m"))))) ")" ))); :: deftheorem defines :::"fComp"::: ENS_1:def 11 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_ens_1 :::"fComp"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_ens_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m2")) ($#k6_ens_1 :::"*"::: ) (Set (Var "m1")))) ")" ) ")" ) ")" ))); definitioncanceled; let "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Ens"::: "V" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: ENS_1:def 13 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" "V" "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) "V" ")" ) "," (Set "(" ($#k8_ens_1 :::"fDom"::: ) "V" ")" ) "," (Set "(" ($#k9_ens_1 :::"fCod"::: ) "V" ")" ) "," (Set "(" ($#k10_ens_1 :::"fComp"::: ) "V" ")" ) "#)" ); end; :: deftheorem ENS_1:def 12 : canceled; :: deftheorem defines :::"Ens"::: ENS_1:def 13 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set (Var "V")) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k8_ens_1 :::"fDom"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k9_ens_1 :::"fCod"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_ens_1 :::"fComp"::: ) (Set (Var "V")) ")" ) "#)" ))); registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_ens_1 :::"Ens"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ; end; theorem :: ENS_1:21 canceled; theorem :: ENS_1:22 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" )))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "V")); func :::"@"::: "A" -> ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) "V" ")" ) equals :: ENS_1:def 14 "A"; end; :: deftheorem defines :::"@"::: ENS_1:def 14 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k12_ens_1 :::"@"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))); theorem :: ENS_1:23 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V"))))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Const "V")) ")" ); func :::"@"::: "a" -> ($#m1_subset_1 :::"Element"::: ) "of" "V" equals :: ENS_1:def 15 "a"; end; :: deftheorem defines :::"@"::: ENS_1:def 15 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set ($#k13_ens_1 :::"@"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))); theorem :: ENS_1:24 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set (Var "m")) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" )))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Const "V"))); func :::"@"::: "m" -> ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) "V" ")" ) equals :: ENS_1:def 16 "m"; end; :: deftheorem defines :::"@"::: ENS_1:def 16 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k14_ens_1 :::"@"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))))); theorem :: ENS_1:25 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Const "V")) ")" ); func :::"@"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) "V") equals :: ENS_1:def 17 "f"; end; :: deftheorem defines :::"@"::: ENS_1:def 17 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set ($#k15_ens_1 :::"@"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); theorem :: ENS_1:26 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ens_1 :::"dom"::: ) (Set "(" ($#k15_ens_1 :::"@"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ens_1 :::"cod"::: ) (Set "(" ($#k15_ens_1 :::"@"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: ENS_1:27 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_ens_1 :::"Maps"::: ) "(" (Set "(" ($#k13_ens_1 :::"@"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k13_ens_1 :::"@"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: ENS_1:28 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_ens_1 :::"@"::: ) (Set (Var "g")) ")" ) ($#k6_ens_1 :::"*"::: ) (Set "(" ($#k15_ens_1 :::"@"::: ) (Set (Var "f")) ")" ))))) ; theorem :: ENS_1:29 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_ens_1 :::"id$"::: ) (Set "(" ($#k13_ens_1 :::"@"::: ) (Set (Var "a")) ")" ))))) ; theorem :: ENS_1:30 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ))) ; theorem :: ENS_1:31 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ENS_1:32 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "W")) ")" ) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ENS_1:33 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ))) ; theorem :: ENS_1:34 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: ENS_1:35 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "W")) ")" ) "st" (Bool (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: ENS_1:36 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) ) "iff" (Bool (Set (Set "(" ($#k15_ens_1 :::"@"::: ) (Set (Var "f")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )))) ; theorem :: ENS_1:37 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "V"))(Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) ")" )))) "holds" (Bool (Set ($#k15_ens_1 :::"@"::: ) (Set (Var "f"))) "is" ($#v1_ens_1 :::"surjective"::: ) )))) ; theorem :: ENS_1:38 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k15_ens_1 :::"@"::: ) (Set (Var "f"))) "is" ($#v1_ens_1 :::"surjective"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) )))) ; theorem :: ENS_1:39 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_ens_1 :::"Ens"::: ) (Set (Var "W")) ")" ) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) )) "holds" (Bool (Set ($#k15_ens_1 :::"@"::: ) (Set (Var "f"))) "is" ($#v1_ens_1 :::"surjective"::: ) )))) ; theorem :: ENS_1:40 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "W"))) "is" ($#v1_cat_2 :::"full"::: ) ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"Hom"::: "C" -> ($#m1_hidden :::"set"::: ) equals :: ENS_1:def 18 "{" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) where a, b "is" ($#m1_subset_1 :::"Object":::) "of" "C" : (Bool verum) "}" ; end; :: deftheorem defines :::"Hom"::: ENS_1:def 18 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) where a, b "is" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool verum) "}" )); registrationlet "C" be ($#l1_cat_1 :::"Category":::); cluster (Set ($#k16_ens_1 :::"Hom"::: ) "C") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ENS_1:41 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")))))) ; theorem :: ENS_1:42 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func :::"hom"::: "(" "a" "," "f" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set "(" ($#k3_graph_1 :::"dom"::: ) "f" ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" ) ")" ")" ) means :: ENS_1:def 19 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set "(" ($#k3_graph_1 :::"dom"::: ) "f" ")" ) ")" ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g"))))); func :::"hom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" ) "," "a" ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) "f" ")" ) "," "a" ")" ")" ) means :: ENS_1:def 20 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" ) "," "a" ")" ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) "f"))); end; :: deftheorem defines :::"hom"::: ENS_1:def 19 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g"))))) ")" ))))); :: deftheorem defines :::"hom"::: ENS_1:def 20 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" ))))); theorem :: ENS_1:43 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ))))) ; theorem :: ENS_1:44 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k18_ens_1 :::"hom"::: ) "(" (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ")" ))))) ; theorem :: ENS_1:45 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "g")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" )))))) ; theorem :: ENS_1:46 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k18_ens_1 :::"hom"::: ) "(" (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: ENS_1:47 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" )))))) ; theorem :: ENS_1:48 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" )))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"hom?-"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) "C" ")" ) ")" ) means :: ENS_1:def 21 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" "a" "," (Set (Var "f")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))); func :::"hom-?"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) "C" ")" ) ")" ) means :: ENS_1:def 22 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," "a" ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," "a" ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," "a" ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"hom?-"::: ENS_1:def 21 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_ens_1 :::"hom?-"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))) ")" )))); :: deftheorem defines :::"hom-?"::: ENS_1:def 22 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_ens_1 :::"hom-?"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))) ")" )))); theorem :: ENS_1:49 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k19_ens_1 :::"hom?-"::: ) (Set (Var "a"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V"))))))) ; theorem :: ENS_1:50 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k20_ens_1 :::"hom-?"::: ) (Set (Var "a"))) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V"))))))) ; theorem :: ENS_1:51 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f9")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f9")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "f", "g" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func :::"hom"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) "g" ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) "f" ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) "g" ")" ) ")" ")" ) means :: ENS_1:def 23 (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) "g" ")" ) ")" ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "g" ($#k1_cat_1 :::"(*)"::: ) (Set (Var "h")) ")" ) ($#k1_cat_1 :::"(*)"::: ) "f"))); end; :: deftheorem defines :::"hom"::: ENS_1:def 23 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "h")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" )))); theorem :: ENS_1:52 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" ))))) ; theorem :: ENS_1:53 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" )) & (Bool (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) ")" )))) ; theorem :: ENS_1:54 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))))) ; theorem :: ENS_1:55 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "g")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ))))) ; theorem :: ENS_1:56 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "," (Set (Var "g9")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f9"))))) "holds" (Bool (Set ($#k21_ens_1 :::"hom"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "g9")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f9")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "g")) "," (Set (Var "g9")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" ))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"hom??"::: "C" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) "C" "," "C" ($#k8_cat_2 :::":]"::: ) )) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) "C" ")" ) ")" ) means :: ENS_1:def 24 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"hom??"::: ENS_1:def 24 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) )) "," (Set "(" ($#k2_ens_1 :::"Maps"::: ) (Set "(" ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k22_ens_1 :::"hom??"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))) ")" ))); theorem :: ENS_1:57 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k19_ens_1 :::"hom?-"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set "(" ($#k22_ens_1 :::"hom??"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k20_ens_1 :::"hom-?"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k22_ens_1 :::"hom??"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ))) ")" ))) ; theorem :: ENS_1:58 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k22_ens_1 :::"hom??"::: ) (Set (Var "C"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "," (Set ($#k11_ens_1 :::"Ens"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Const "C"))) ($#r1_tarski :::"c="::: ) (Set (Const "V"))) ; func :::"hom?-"::: "(" "V" "," "a" ")" -> ($#m2_cat_1 :::"Functor"::: ) "of" "C" "," (Set ($#k11_ens_1 :::"Ens"::: ) "V") equals :: ENS_1:def 25 (Set ($#k19_ens_1 :::"hom?-"::: ) "a"); func :::"hom-?"::: "(" "V" "," "a" ")" -> ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" "C" "," (Set ($#k11_ens_1 :::"Ens"::: ) "V") equals :: ENS_1:def 26 (Set ($#k20_ens_1 :::"hom-?"::: ) "a"); end; :: deftheorem defines :::"hom?-"::: ENS_1:def 25 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k23_ens_1 :::"hom?-"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k19_ens_1 :::"hom?-"::: ) (Set (Var "a"))))))); :: deftheorem defines :::"hom-?"::: ENS_1:def 26 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k24_ens_1 :::"hom-?"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_ens_1 :::"hom-?"::: ) (Set (Var "a"))))))); definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#l1_cat_1 :::"Category":::); assume (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Const "C"))) ($#r1_tarski :::"c="::: ) (Set (Const "V"))) ; func :::"hom??"::: "(" "V" "," "C" ")" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" ) "," "C" ($#k8_cat_2 :::":]"::: ) ) "," (Set ($#k11_ens_1 :::"Ens"::: ) "V") equals :: ENS_1:def 27 (Set ($#k22_ens_1 :::"hom??"::: ) "C"); end; :: deftheorem defines :::"hom??"::: ENS_1:def 27 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k25_ens_1 :::"hom??"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k22_ens_1 :::"hom??"::: ) (Set (Var "C")))))); theorem :: ENS_1:59 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k23_ens_1 :::"hom?-"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k17_ens_1 :::"hom"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: ENS_1:60 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k23_ens_1 :::"hom?-"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: ENS_1:61 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k24_ens_1 :::"hom-?"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k18_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: ENS_1:62 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k24_ens_1 :::"hom-?"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))))) ; theorem :: ENS_1:63 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k25_ens_1 :::"hom??"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k10_cat_2 :::"["::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" ) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k21_ens_1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ; theorem :: ENS_1:64 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k25_ens_1 :::"hom??"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set (Var "b")) ($#k9_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: ENS_1:65 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k25_ens_1 :::"hom??"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k12_cat_2 :::"?-"::: ) (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k23_ens_1 :::"hom?-"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ))))) ; theorem :: ENS_1:66 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k16_ens_1 :::"Hom"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k25_ens_1 :::"hom??"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ")" ) ($#k13_cat_2 :::"-?"::: ) (Set (Var "a"))) ($#r1_funct_2 :::"="::: ) (Set ($#k24_ens_1 :::"hom-?"::: ) "(" (Set (Var "V")) "," (Set (Var "a")) ")" ))))) ;