:: FUNCOP_1 semantic presentation begin theorem :: FUNCOP_1:1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_funct_3 :::"delta"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k13_funct_3 :::":>"::: ) ))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func "f" :::"~"::: -> ($#m1_hidden :::"Function":::) means :: FUNCOP_1:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ) & (Bool "(" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) "or" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" ) ")" ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ) & (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) "or" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ) & (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) "or" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" ) ")" )) ; end; :: deftheorem defines :::"~"::: FUNCOP_1:def 1 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funcop_1 :::"~"::: ) )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ) & (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) "or" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" ) ")" ) ")" )); theorem :: FUNCOP_1:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k13_funct_3 :::":>"::: ) ) ($#k1_funcop_1 :::"~"::: ) ))) ; theorem :: FUNCOP_1:3 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funcop_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funcop_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: FUNCOP_1:4 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k12_funct_3 :::"delta"::: ) (Set (Var "A")) ")" ) ($#k1_funcop_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_funct_3 :::"delta"::: ) (Set (Var "A"))))) ; theorem :: FUNCOP_1:5 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) )))) ; theorem :: FUNCOP_1:6 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set "(" (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k13_funct_3 :::":>"::: ) )))) ; definitionlet "A", "z" be ($#m1_hidden :::"set"::: ) ; func "A" :::"-->"::: "z" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 2 (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," (Set ($#k1_tarski :::"{"::: ) "z" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); end; :: deftheorem defines :::"-->"::: FUNCOP_1:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))); registrationlet "A", "z" be ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k2_funcop_1 :::"-->"::: ) "z") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCOP_1:7 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: FUNCOP_1:8 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: FUNCOP_1:9 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")))))) ; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FUNCOP_1:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCOP_1:11 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")))))) ; theorem :: FUNCOP_1:12 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x"))))) ; theorem :: FUNCOP_1:13 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" )) ; theorem :: FUNCOP_1:14 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: FUNCOP_1:15 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: FUNCOP_1:16 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCOP_1:17 (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: FUNCOP_1:18 (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FUNCOP_1:19 (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k8_relat_1 :::"""::: ) (Set (Var "A")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")))))) ; theorem :: FUNCOP_1:20 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k1_funcop_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )))) ; definitionlet "F", "f", "g" be ($#m1_hidden :::"Function":::); func "F" :::".:"::: "(" "f" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 3 (Set "F" ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) )); end; :: deftheorem defines :::".:"::: FUNCOP_1:def 3 : (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) )))); registrationlet "F", "f", "g" be ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k3_funcop_1 :::".:"::: ) "(" "f" "," "g" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCOP_1:21 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "F")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ; theorem :: FUNCOP_1:22 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: FUNCOP_1:23 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))))) ; theorem :: FUNCOP_1:24 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "h")) "," (Set (Var "f")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "h")) "," (Set (Var "g")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))))) ; theorem :: FUNCOP_1:25 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ))) ; definitionlet "F", "f" be ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; func "F" :::"[:]"::: "(" "f" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 4 (Set "F" ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) "f" "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_funcop_1 :::"-->"::: ) "x" ")" ) ($#k13_funct_3 :::":>"::: ) )); end; :: deftheorem defines :::"[:]"::: FUNCOP_1:def 4 : (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k13_funct_3 :::":>"::: ) ))))); registrationlet "F", "f" be ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k4_funcop_1 :::"[:]"::: ) "(" "f" "," "x" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCOP_1:26 (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: FUNCOP_1:27 (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "z")) ")" )))) ; theorem :: FUNCOP_1:28 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "g")) "," (Set (Var "x")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))))) ; theorem :: FUNCOP_1:29 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set (Var "x")) ")" )))) ; theorem :: FUNCOP_1:30 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) "," (Set (Var "x")) ")" )))))) ; definitionlet "F" be ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_hidden :::"Function":::); func "F" :::"[;]"::: "(" "x" "," "g" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 5 (Set "F" ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ($#k2_funcop_1 :::"-->"::: ) "x" ")" ) "," "g" ($#k13_funct_3 :::":>"::: ) )); end; :: deftheorem defines :::"[;]"::: FUNCOP_1:def 5 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) )))))); registrationlet "F" be ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k5_funcop_1 :::"[;]"::: ) "(" "x" "," "g" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCOP_1:31 (Bool "for" (Set (Var "g")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) "," (Set (Var "g")) ")" )))) ; theorem :: FUNCOP_1:32 (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "z")) "," (Set (Var "f")) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "z")) "," (Set (Var "f")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: FUNCOP_1:33 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "g")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))))) ; theorem :: FUNCOP_1:34 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUNCOP_1:35 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" )))))) ; theorem :: FUNCOP_1:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X"))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "f", "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Z")) "," (Set (Const "X")); :: original: :::".:"::: redefine func "F" :::".:"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Z" "," "X"; end; theorem :: FUNCOP_1:37 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) ")" )))))) ; theorem :: FUNCOP_1:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))))) ; theorem :: FUNCOP_1:39 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "g")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))) ; theorem :: FUNCOP_1:40 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "f")) ")" )))))) ; theorem :: FUNCOP_1:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ))))) ; theorem :: FUNCOP_1:42 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "g")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: FUNCOP_1:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "x")) ")" )))))) ; theorem :: FUNCOP_1:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ))))) ; theorem :: FUNCOP_1:45 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_funcop_1 :::"-->"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")))) ; definitionlet "I", "i" be ($#m1_hidden :::"set"::: ) ; :: original: :::"-->"::: redefine func "I" :::"-->"::: "i" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set ($#k1_tarski :::"{"::: ) "i" ($#k1_tarski :::"}"::: ) ); end; definitionlet "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); :: original: :::"-->"::: redefine func "A" :::"-->"::: "b" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; theorem :: FUNCOP_1:46 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "X")))))) ; theorem :: FUNCOP_1:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Z")) "," (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"[:]"::: redefine func "F" :::"[:]"::: "(" "f" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Z" "," "X"; end; theorem :: FUNCOP_1:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) "," (Set (Var "x")) ")" ))))))) ; theorem :: FUNCOP_1:49 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )))))) ; theorem :: FUNCOP_1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )))))) ; theorem :: FUNCOP_1:51 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ))))) ; theorem :: FUNCOP_1:52 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "g")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Z")) "," (Set (Const "X")); :: original: :::"[;]"::: redefine func "F" :::"[;]"::: "(" "x" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Z" "," "X"; end; theorem :: FUNCOP_1:53 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ))))))) ; theorem :: FUNCOP_1:54 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" )))))) ; theorem :: FUNCOP_1:55 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ))))))) ; theorem :: FUNCOP_1:56 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ))))) ; theorem :: FUNCOP_1:57 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funcop_1 :::"~"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ))))) ; definitionlet "X", "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "Y")) "," (Set (Const "Z")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"proj2"::: redefine func :::"rng"::: "f" -> ($#m1_subset_1 :::"Relation":::) "of" "Y" "," "Z"; end; definitionlet "X", "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "Y")) "," (Set (Const "Z")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"~"::: redefine func "f" :::"~"::: -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "Z" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ); end; theorem :: FUNCOP_1:58 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k11_funcop_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k12_funcop_1 :::"~"::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k11_funcop_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k3_relset_1 :::"~"::: ) )))) ; theorem :: FUNCOP_1:59 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x1")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "x2")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x1")) "," (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x2")) ")" ")" ) ")" ))))))) ; theorem :: FUNCOP_1:60 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "g")) ")" ")" ) ")" ))))))) ; theorem :: FUNCOP_1:61 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" )))))) ; theorem :: FUNCOP_1:62 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x1")) "," (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x2")) "," (Set (Var "f")) ")" ")" ) ")" ))))))) ; theorem :: FUNCOP_1:63 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x1")) ")" ")" ) "," (Set (Var "x2")) ")" ))))))) ; theorem :: FUNCOP_1:64 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))))))) ; theorem :: FUNCOP_1:65 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))))) ; theorem :: FUNCOP_1:66 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))))) ; theorem :: FUNCOP_1:67 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) "," (Set (Var "f")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))))))) ; theorem :: FUNCOP_1:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))))))) ; theorem :: FUNCOP_1:69 (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) ; definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"Function-yielding"::: means :: FUNCOP_1:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"Function-yielding"::: FUNCOP_1:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "B" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); let "j" be ($#m1_hidden :::"set"::: ) ; cluster (Set "B" ($#k1_funct_1 :::"."::: ) "j") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "F" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); let "f" be ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "F") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "B" be ($#m1_hidden :::"set"::: ) ; let "c" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "B" ($#k2_funcop_1 :::"-->"::: ) "c") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; theorem :: FUNCOP_1:70 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "z"))))))) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func "(" "a" "," "b" ")" :::".-->"::: "c" -> ($#m1_hidden :::"Function":::) equals :: FUNCOP_1:def 7 (Set (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "c"); end; :: deftheorem defines :::".-->"::: FUNCOP_1:def 7 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c"))))); theorem :: FUNCOP_1:71 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "c")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; definitionlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"IFEQ"::: "(" "x" "," "y" "," "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 8 "a" if (Bool "x" ($#r1_hidden :::"="::: ) "y") otherwise "b"; end; :: deftheorem defines :::"IFEQ"::: FUNCOP_1:def 8 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "implies" (Bool (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) "implies" (Bool (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"IFEQ"::: redefine func :::"IFEQ"::: "(" "x" "," "y" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; func "x" :::".-->"::: "y" -> ($#m1_hidden :::"set"::: ) equals :: FUNCOP_1:def 9 (Set (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "y"); end; :: deftheorem defines :::".-->"::: FUNCOP_1:def 9 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y"))))); registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: FUNCOP_1:72 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: FUNCOP_1:73 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ))) ; notationlet "o", "m", "r" be ($#m1_hidden :::"set"::: ) ; synonym "(" "o" "," "m" ")" :::":->"::: "r" for "(" "o" "," "m" ")" :::".-->"::: "r"; end; definitionlet "o", "m", "r" be ($#m1_hidden :::"set"::: ) ; :: original: :::".-->"::: redefine func "(" "o" "," "m" ")" :::":->"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) "o" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "m" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "r" ($#k1_tarski :::"}"::: ) ) means :: FUNCOP_1:def 10 (Bool verum); end; :: deftheorem defines :::":->"::: FUNCOP_1:def 10 : (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "," (Set (Var "r")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "o")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "m")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "o")) "," (Set (Var "m")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "r")))) "iff" (Bool verum) ")" ))); theorem :: FUNCOP_1:74 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )))) ; theorem :: FUNCOP_1:75 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: FUNCOP_1:76 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; notationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; synonym "x" :::":->"::: "y" for "x" :::".-->"::: "y"; end; definitionlet "m", "o" be ($#m1_hidden :::"set"::: ) ; :: original: :::".-->"::: redefine func "m" :::":->"::: "o" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) "m" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "o" ($#k1_tarski :::"}"::: ) ); end; theorem :: FUNCOP_1:77 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "c")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "c")))))) ; registrationlet "f" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); let "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "C") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); cluster (Set "A" ($#k2_funcop_1 :::"-->"::: ) "f") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "X", "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "a") -> ($#v3_funct_1 :::"constant"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v3_funct_1 :::"constant"::: ) ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v3_funct_1 :::"constant"::: ) ; end; theorem :: FUNCOP_1:78 (Bool "for" (Set (Var "f")) "being" ($#v3_funct_1 :::"constant"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: FUNCOP_1:79 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: FUNCOP_1:80 (Bool "for" (Set (Var "f")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "f")) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "I", "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "A") -> "I" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I", "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set "I" ($#k16_funcop_1 :::".-->"::: ) "A") -> (Set ($#k1_tarski :::"{"::: ) "I" ($#k1_tarski :::"}"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; theorem :: FUNCOP_1:81 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); cluster (Set "I" ($#k16_funcop_1 :::".-->"::: ) "f") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FUNCOP_1:82 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y"))) ($#r3_wellord1 :::"is_isomorphism_of"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: FUNCOP_1:83 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#r4_wellord1 :::"are_isomorphic"::: ) )) ; registrationlet "I", "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set "I" ($#k2_funcop_1 :::"-->"::: ) "A") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; theorem :: FUNCOP_1:84 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "f"))))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "i") -> "A" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: FUNCOP_1:85 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))))))) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); cluster (Set "A" ($#k2_funcop_1 :::"-->"::: ) "x") -> "B" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> "A" ($#v4_relat_1 :::"-defined"::: ) ; end; theorem :: FUNCOP_1:86 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y"))))) ; registrationlet "Y" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"Relation-yielding"::: means :: FUNCOP_1:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Relation":::))); end; :: deftheorem defines :::"Relation-yielding"::: FUNCOP_1:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_funcop_1 :::"Relation-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Relation":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) -> ($#v2_funcop_1 :::"Relation-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FUNCOP_1:87 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) ")" ) ")" )) ; theorem :: FUNCOP_1:88 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: FUNCOP_1:89 (Bool "for" (Set (Var "z")) "," (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x"))))) ;