:: FUNCT_7 semantic presentation begin theorem :: FUNCT_7:1 (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_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_7:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "B")))))))) ; theorem :: FUNCT_7:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: FUNCT_7:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B")) ")" )))))))) ; theorem :: FUNCT_7:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B")) ")" )))))))) ; theorem :: FUNCT_7:6 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))))) ; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "x" "," "y" ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FUNCT_7:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "i")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k5_relat_1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: FUNCT_7:8 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k17_funcop_1 :::":->"::: ) (Set "(" (Set (Var "M")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k5_relat_1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "j")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))))) ; theorem :: FUNCT_7:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" )))) ; theorem :: FUNCT_7:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )))) ; theorem :: FUNCT_7:11 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) ; theorem :: FUNCT_7:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "B")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "A")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ")" )))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ; theorem :: FUNCT_7:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ))))) ; theorem :: FUNCT_7:14 (Bool "for" (Set (Var "X")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: FUNCT_7:15 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ))))) ; theorem :: FUNCT_7:16 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set ($#k4_numbers :::"INT"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) ; theorem :: FUNCT_7:17 (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: FUNCT_7:18 (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) )) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ; theorem :: FUNCT_7:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) ; theorem :: FUNCT_7:20 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#m1_hidden :::"Cardinal":::))) ; theorem :: FUNCT_7:21 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "C")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))))) ; theorem :: FUNCT_7:22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) ")" ) ")" ))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "f" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; let "g" be ($#m1_hidden :::"Function":::); cluster (Set ($#k10_finseq_1 :::"<*"::: ) "f" "," "g" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; let "h" be ($#m1_hidden :::"Function":::); cluster (Set ($#k11_finseq_1 :::"<*"::: ) "f" "," "g" "," "h" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_hidden :::"Function":::); cluster (Set "n" ($#k2_finseq_2 :::"|->"::: ) "f") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "p", "q" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; theorem :: FUNCT_7:23 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ) ")" )) ; begin scheme :: FUNCT_7:sch 1 Kappa2D{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )))) proof end; scheme :: FUNCT_7:sch 2 FinMono{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set F4 "(" (Set (Var "d")) ")" ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F1 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set F4 "(" (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "d2")) ")" ))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2")))) proof end; scheme :: FUNCT_7:sch 3 CardMono{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F1 "(" ")" ) "," "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set F3 "(" (Set (Var "d")) ")" ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" ($#r2_wellord2 :::"are_equipotent"::: ) ) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d")) ")" )))) and (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set F3 "(" (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d2")) ")" ))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2")))) proof end; scheme :: FUNCT_7:sch 4 CardMono9{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F1 "(" ")" ) "," "{" (Set F3 "(" (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" ($#r2_wellord2 :::"are_equipotent"::: ) ) provided (Bool (Set F1 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) and (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set F3 "(" (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d2")) ")" ))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2")))) proof end; scheme :: FUNCT_7:sch 5 FuncSeqInd{ P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool P1[(Set ($#k1_xboole_0 :::"{}"::: ) )]) and (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool P1[(Set (Var "p"))])) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool P1[(Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ))]))) proof end; begin definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set (Const "y"))) ; func :::"In"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "y" equals :: FUNCT_7:def 1 "x"; end; :: deftheorem defines :::"In"::: FUNCT_7:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_funct_7 :::"In"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))); theorem :: FUNCT_7:24 (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_funct_7 :::"In"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_7 :::"In"::: ) "(" (Set (Var "x")) "," (Set (Var "B")) ")" ))) ; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); let "A" be ($#m1_hidden :::"set"::: ) ; pred "f" "," "g" :::"equal_outside"::: "A" means :: FUNCT_7:def 2 (Bool (Set "f" ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k6_subset_1 :::"\"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set "g" ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ($#k6_subset_1 :::"\"::: ) "A" ")" ))); end; :: deftheorem defines :::"equal_outside"::: FUNCT_7:def 2 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))) "iff" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" ))) ")" ))); theorem :: FUNCT_7:25 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "f")) "," (Set (Var "f")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:26 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "g")) "," (Set (Var "f")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:27 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) "," (Set (Var "h")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) "," (Set (Var "h")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:28 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_7:29 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) "," (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); let "i", "x" be ($#m1_hidden :::"set"::: ) ; func "f" :::"+*"::: "(" "i" "," "x" ")" -> ($#m1_hidden :::"Function":::) equals :: FUNCT_7:def 3 (Set "f" ($#k1_funct_4 :::"+*"::: ) (Set "(" "i" ($#k16_funcop_1 :::".-->"::: ) "x" ")" )) if (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) otherwise "f"; end; :: deftheorem defines :::"+*"::: FUNCT_7:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "i")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ")" ))); theorem :: FUNCT_7:30 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_7:31 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ; theorem :: FUNCT_7:32 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: FUNCT_7:33 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "j")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "j")) "," (Set (Var "e")) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" )))) ; theorem :: FUNCT_7:34 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "e")) ")" )))) ; theorem :: FUNCT_7:35 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; registrationlet "f" be ($#m1_hidden :::"FinSequence":::); let "i", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "i" "," "x" ")" ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"+*"::: redefine func "f" :::"+*"::: "(" "i" "," "d" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: FUNCT_7:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: FUNCT_7:37 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")))))))) ; theorem :: FUNCT_7:38 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::); func :::"compose"::: "(" "p" "," "X" ")" -> ($#m1_hidden :::"Function":::) means :: FUNCT_7:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) "X")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))))) ")" ) ")" )); end; :: deftheorem defines :::"compose"::: FUNCT_7:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))))) ")" ) ")" )) ")" )))); definitionlet "p" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; func :::"apply"::: "(" "p" "," "x" ")" -> ($#m1_hidden :::"FinSequence":::) means :: FUNCT_7:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "x") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"apply"::: FUNCT_7:def 5 : (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ) ")" ) ")" )))); theorem :: FUNCT_7:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))))) ; theorem :: FUNCT_7:40 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: FUNCT_7:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" )))))) ; theorem :: FUNCT_7:42 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))))) ; theorem :: FUNCT_7:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )))))) ; theorem :: FUNCT_7:44 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ")" )))))) ; theorem :: FUNCT_7:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ))))) ; theorem :: FUNCT_7:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_7:47 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ; theorem :: FUNCT_7:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "q")) "," (Set (Var "Y")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" ))))) ; theorem :: FUNCT_7:49 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: FUNCT_7:50 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ))))) ; theorem :: FUNCT_7:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ))))) ; theorem :: FUNCT_7:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "or" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_7:53 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k11_finseq_1 :::"*>"::: ) )))) ; theorem :: FUNCT_7:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ))))) ; theorem :: FUNCT_7:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "or" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "or" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_7:56 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_funct_7 :::"apply"::: ) "(" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))))) ; definitionlet "F" be ($#m1_hidden :::"FinSequence":::); func :::"firstdom"::: "F" -> ($#m1_hidden :::"set"::: ) means :: FUNCT_7:def 6 (Bool it "is" ($#v1_xboole_0 :::"empty"::: ) ) if (Bool "F" "is" ($#v1_xboole_0 :::"empty"::: ) ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))); func :::"lastrng"::: "F" -> ($#m1_hidden :::"set"::: ) means :: FUNCT_7:def 7 (Bool it "is" ($#v1_xboole_0 :::"empty"::: ) ) if (Bool "F" "is" ($#v1_xboole_0 :::"empty"::: ) ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ) ")" ))); end; :: deftheorem defines :::"firstdom"::: FUNCT_7:def 6 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b2")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) ")" ) ")" ")" ))); :: deftheorem defines :::"lastrng"::: FUNCT_7:def 7 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b2")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ")" ))) ")" ) ")" ")" ))); theorem :: FUNCT_7:57 (Bool "(" (Bool (Set ($#k6_funct_7 :::"firstdom"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FUNCT_7:58 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k6_funct_7 :::"firstdom"::: ) (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ; theorem :: FUNCT_7:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "p")))))) ; definitionlet "IT" be ($#m1_hidden :::"FinSequence":::); attr "IT" is :::"FuncSeq-like"::: means :: FUNCT_7:def 8 (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "IT" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"FuncSeq-like"::: FUNCT_7:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_funct_7 :::"FuncSeq-like"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" )) ")" )); theorem :: FUNCT_7:60 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v1_funct_7 :::"FuncSeq-like"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_funct_7 :::"FuncSeq-like"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_funct_7 :::"FuncSeq-like"::: ) ) ")" )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funct_7 :::"FuncSeq-like"::: ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> ($#v1_funct_7 :::"FuncSeq-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"Function":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "f" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_funct_7 :::"FuncSeq-like"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_funct_7 :::"FuncSeq-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode FuncSequence is ($#v1_funct_7 :::"FuncSeq-like"::: ) ($#m1_hidden :::"FinSequence":::); end; theorem :: FUNCT_7:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FuncSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_7:62 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FuncSequence":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p"))))) ; theorem :: FUNCT_7:63 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FuncSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) "is" ($#m1_hidden :::"FuncSequence":::)))) ; theorem :: FUNCT_7:64 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FuncSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) )) "is" ($#m1_hidden :::"FuncSequence":::)))) ; theorem :: FUNCT_7:65 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FuncSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k5_funct_7 :::"apply"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set (Var "X")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; assume "(" (Bool (Bool (Set (Const "Y")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ; mode :::"FuncSequence"::: "of" "X" "," "Y" -> ($#m1_hidden :::"FuncSequence":::) means :: FUNCT_7:def 9 (Bool "(" (Bool (Set ($#k6_funct_7 :::"firstdom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) it) ($#r1_tarski :::"c="::: ) "Y") ")" ); end; :: deftheorem defines :::"FuncSequence"::: FUNCT_7:def 9 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FuncSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_funct_7 :::"FuncSequence"::: ) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_funct_7 :::"FuncSequence"::: ) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"compose"::: redefine func :::"compose"::: "(" "F" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "Y"; end; definitionlet "q" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::); mode :::"FuncSequence"::: "of" "q" -> ($#m1_hidden :::"FinSequence":::) means :: FUNCT_7:def 10 (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "q")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"FuncSequence"::: FUNCT_7:def 10 : (Bool "for" (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_funct_7 :::"FuncSequence"::: ) "of" (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" ) ")" ))); registrationlet "q" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::); cluster -> ($#v2_relat_1 :::"non-empty"::: ) ($#v1_funct_7 :::"FuncSeq-like"::: ) for ($#m2_funct_7 :::"FuncSequence"::: ) "of" "q"; end; theorem :: FUNCT_7:66 (Bool "for" (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#m2_funct_7 :::"FuncSequence"::: ) "of" (Set (Var "q")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_funct_7 :::"firstdom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k7_funct_7 :::"lastrng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ))) ")" ))) ; theorem :: FUNCT_7:67 (Bool "for" (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#m2_funct_7 :::"FuncSequence"::: ) "of" (Set (Var "q")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ))) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "n") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; definitionlet "f" be ($#m1_hidden :::"Relation":::); let "n" be ($#m1_hidden :::"Nat":::); func :::"iter"::: "(" "f" "," "n" ")" -> ($#m1_hidden :::"Relation":::) means :: FUNCT_7:def 11 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) "f" ")" ) "," (Set "(" ($#k1_relat_1 :::"field"::: ) "f" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) "f" ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"iter"::: FUNCT_7:def 11 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "f")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ) ")" )) ")" )))); registrationlet "f" be ($#m1_hidden :::"Function":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k9_funct_7 :::"iter"::: ) "(" "f" "," "n" ")" ) -> ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_7:68 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" )))) ; theorem :: FUNCT_7:69 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" ))))) ; theorem :: FUNCT_7:70 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "R")))) ; theorem :: FUNCT_7:71 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; theorem :: FUNCT_7:72 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) ")" ))) ; theorem :: FUNCT_7:73 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" ))) ; theorem :: FUNCT_7:74 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) ")" ))) ; theorem :: FUNCT_7:75 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" )))) ; theorem :: FUNCT_7:76 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" )))) ; theorem :: FUNCT_7:77 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "m")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: FUNCT_7:78 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "m")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" )))) ; theorem :: FUNCT_7:79 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "m")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" )))) ; theorem :: FUNCT_7:80 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCT_7:81 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_7:82 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "R")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCT_7:83 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")))))) ; theorem :: FUNCT_7:84 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_7:85 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "m")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ))))) ; theorem :: FUNCT_7:86 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X")))))) ; theorem :: FUNCT_7:87 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: FUNCT_7:88 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_relat_1 :::"field"::: ) (Set (Var "f")) ")" ) ")" )))) ; begin theorem :: FUNCT_7:89 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "f"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))))) "holds" (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: FUNCT_7:90 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "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")))) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_7:91 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) "," (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:92 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FUNCT_7:93 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "A")) "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")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_7:94 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: FUNCT_7:95 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k2_funct_7 :::"+*"::: ) "(" (Num 1) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: FUNCT_7:96 (Bool "for" (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 (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_7:97 (Bool "for" (Set (Var "w")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "w")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w"))))))) ; theorem :: FUNCT_7:98 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Set (Var "w")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "w")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "w")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ))))))) ; definitionlet "F" be ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; func :::"Swap"::: "(" "F" "," "x" "," "y" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_7:def 12 (Set (Set "(" "F" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) "y" ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" "y" "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) "x" ")" ) ")" ) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) ")" ) otherwise "F"; end; :: deftheorem defines :::"Swap"::: FUNCT_7:def 12 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "implies" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) ")" )) "implies" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F"))) ")" ")" ))); registrationlet "F" be ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "F" "," "x" "," "y" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_7:99 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))))) ; theorem :: FUNCT_7:100 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: FUNCT_7:101 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: FUNCT_7:102 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: FUNCT_7:103 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))))) ; scheme :: FUNCT_7:sch 6 Sch6{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F1 "(" ")" ) "," "{" (Set F3 "(" (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" ($#r2_wellord2 :::"are_equipotent"::: ) ) provided (Bool (Set F1 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) and (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "d1")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "d2")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set F3 "(" (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d2")) ")" ))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2")))) proof end; theorem :: FUNCT_7:104 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) "," (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:105 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))) "," (Set (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:106 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")))) "iff" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) ")" )) ; theorem :: FUNCT_7:107 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))) ; theorem :: FUNCT_7:108 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" ) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: FUNCT_7:109 (Bool "for" (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 (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_7:110 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")))))) ; theorem :: FUNCT_7:111 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "st" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))))))) ; theorem :: FUNCT_7:112 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "," (Set (Var "r")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "d")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "r")) ")" ) ")" ))))) ; theorem :: FUNCT_7:113 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "m")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ")" ) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "m"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))) ; theorem :: FUNCT_7:114 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "A")) "," (Set (Var "b")) "," (Set (Var "B")) "," (Set (Var "c")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "b")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "c")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:115 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))))) ; theorem :: FUNCT_7:116 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))))) ; theorem :: FUNCT_7:117 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "g")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; definitionlet "a", "b" be ($#m1_hidden :::"set"::: ) ; func "a" :::"followed_by"::: "b" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_7:def 13 (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "b" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," "a" ")" ); end; :: deftheorem defines :::"followed_by"::: FUNCT_7:def 13 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "b")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ")" ))); registrationlet "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set "a" ($#k11_funct_7 :::"followed_by"::: ) "b") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_7:118 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"followed_by"::: redefine func "a" :::"followed_by"::: "b" -> ($#m1_subset_1 :::"sequence":::) "of" "X"; end; theorem :: FUNCT_7:119 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "b")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: FUNCT_7:120 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "b")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; definitionlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; func "(" "a" "," "b" ")" :::"followed_by"::: "c" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_7:def 14 (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "c" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ")" )); end; :: deftheorem defines :::"followed_by"::: FUNCT_7:def 14 : (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_funct_7 :::"followed_by"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )))); registrationlet "a", "b", "c" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "a" "," "b" ")" ($#k13_funct_7 :::"followed_by"::: ) "c") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_7:121 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: FUNCT_7:122 (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_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: FUNCT_7:123 (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_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: FUNCT_7:124 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: FUNCT_7:125 (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_funct_7 :::"followed_by"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Num 1) "," (Set (Var "b")) ")" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b", "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"followed_by"::: redefine func "(" "a" "," "b" ")" :::"followed_by"::: "c" -> ($#m1_subset_1 :::"sequence":::) "of" "X"; end; theorem :: FUNCT_7:126 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "a")) ($#k11_funct_7 :::"followed_by"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FUNCT_7:127 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k13_funct_7 :::"followed_by"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) ))) ; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); :: original: :::"+*"::: redefine func "f" :::"+*"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; theorem :: FUNCT_7:128 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; theorem :: FUNCT_7:129 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k15_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: FUNCT_7:130 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "," (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_7:131 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:132 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))) "," (Set (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_7:133 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "I")))))) ; theorem :: FUNCT_7:134 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:135 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B")))))) ; theorem :: FUNCT_7:136 (Bool "for" (Set (Var "I")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "X")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A"))))) ; theorem :: FUNCT_7:137 (Bool "for" (Set (Var "B")) "," (Set (Var "I")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_funct_7 :::"equal_outside"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "X")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B")))))) ; registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "V")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "V")); cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ) -> "V" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: FUNCT_7:138 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: FUNCT_7:139 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "l1")) "," (Set (Var "l2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "l1")) "," (Set (Var "i1")) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "l2")) "," (Set (Var "i2")) ")" )))))) ;