:: CARD_FIN semantic presentation begin theorem :: CARD_FIN:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; theorem :: CARD_FIN:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) : (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) "}" )))) ; theorem :: CARD_FIN:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) : (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "}" )))) ; theorem :: CARD_FIN:4 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k13_newton :::"|^"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" )))) ; theorem :: CARD_FIN:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (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"::: ) ) ")" & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) : (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) "}" )))) ; theorem :: CARD_FIN:6 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k9_newton :::"!"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k9_newton :::"!"::: ) ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: CARD_FIN:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) : (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "}" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k9_newton :::"!"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ")" ) ($#k9_newton :::"!"::: ) ")" )))) ; theorem :: CARD_FIN:8 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) : (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))) "}" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k9_newton :::"!"::: ) ))) ; definitionlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_hidden :::"Nat":::); let "x1", "x2" be ($#m1_hidden :::"set"::: ) ; func :::"Choose"::: "(" "X" "," "k" "," "x1" "," "x2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "X" "," (Set ($#k2_tarski :::"{"::: ) "x1" "," "x2" ($#k2_tarski :::"}"::: ) ) ")" ")" ) means :: CARD_FIN:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k2_tarski :::"{"::: ) "x1" "," "x2" ($#k2_tarski :::"}"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) "x1" ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) "k") ")" )) ")" )); end; :: deftheorem defines :::"Choose"::: CARD_FIN:def 1 : (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x1")) "," (Set (Var "x2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )) ")" )) ")" ))))); theorem :: CARD_FIN:9 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x1")) "," (Set (Var "x1")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: CARD_FIN:10 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x1")) "," (Set (Var "x2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: CARD_FIN:11 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: CARD_FIN:12 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: CARD_FIN:13 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) : (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) "}" ))))) ; theorem :: CARD_FIN:14 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) : (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) "}" ))))) ; theorem :: CARD_FIN:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )))))) ; theorem :: CARD_FIN:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k6_newton :::"choose"::: ) (Set (Var "k"))))))) ; theorem :: CARD_FIN:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; definitionlet "F", "Ch" be ($#m1_hidden :::"Function":::); let "y" be ($#m1_hidden :::"set"::: ) ; func :::"Intersection"::: "(" "F" "," "Ch" "," "y" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "F" ")" ) ")" ) means :: CARD_FIN:def 2 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "F" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "Ch")) & (Bool (Set "Ch" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "y")) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Intersection"::: CARD_FIN:def 2 : (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Ch")))) & (Bool (Set (Set (Var "Ch")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ")" )) ")" )))); theorem :: CARD_FIN:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Ch")))) & (Bool (Set (Set (Var "Ch")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))) ")" ))) ; theorem :: CARD_FIN:20 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))))) ; theorem :: CARD_FIN:21 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))))))) ; theorem :: CARD_FIN:22 (Bool "for" (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Ch"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Ch")))) & (Bool (Set (Set (Var "Ch")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: CARD_FIN:23 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ))))) ; theorem :: CARD_FIN:24 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ))))) ; theorem :: CARD_FIN:25 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ))))) ; theorem :: CARD_FIN:26 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ))))) ; theorem :: CARD_FIN:27 (Bool "for" (Set (Var "y")) "," (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "Ch")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X9")) ")" ) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:28 (Bool "for" (Set (Var "y")) "," (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Ch")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X9")) ")" ) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "Ch")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X9")) ")" ) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:29 (Bool "for" (Set (Var "X9")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X9")) ")" ) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:30 (Bool "for" (Set (Var "y")) "," (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Ch")))) & (Bool (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "X9")))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X9")) ")" ) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: CARD_FIN:32 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "Ch")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Ch")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "," (Set (Var "y")) ")" ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:33 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch1")) "," (Set (Var "Ch2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "Ch1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Ch2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch1")) "," (Set (Var "x1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch2")) "," (Set (Var "x2")) ")" )))) ; theorem :: CARD_FIN:34 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ))))) ; theorem :: CARD_FIN:35 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: CARD_FIN:36 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Ch")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ))))) ; theorem :: CARD_FIN:37 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))) ")" ))) ; registrationlet "F" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v2_finset_1 :::"finite-yielding"::: ) ; end; registrationlet "F" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::); let "G" be ($#m1_hidden :::"Function":::); cluster (Set "G" ($#k3_relat_1 :::"(#)"::: ) "F") -> ($#v2_finset_1 :::"finite-yielding"::: ) ; cluster (Set ($#k1_yellow20 :::"Intersect"::: ) "(" "F" "," "G" ")" ) -> ($#v2_finset_1 :::"finite-yielding"::: ) ; end; theorem :: CARD_FIN:38 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Ch"))))) "holds" (Bool (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: CARD_FIN:39 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Fy")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: CARD_FIN:40 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "n")) "," (Set (Var "k")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )) ")" ))) ; definitioncanceled; let "k" be ($#m1_hidden :::"Nat":::); let "F" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::); assume (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "F"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ; func :::"Card_Intersection"::: "(" "F" "," "k" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: CARD_FIN:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," "k" "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) "," (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," "k" "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "F") ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "P")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_recdef_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" "F" "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XFS")))) ")" ))))); end; :: deftheorem CARD_FIN:def 3 : canceled; :: deftheorem defines :::"Card_Intersection"::: CARD_FIN:def 4 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) "," (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "P")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_recdef_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )))) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XFS")))) ")" ))))) ")" )))); theorem :: CARD_FIN:41 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) "," (Set "(" ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "P")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_recdef_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )))) ")" )) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XFS")))))))))) ; theorem :: CARD_FIN:42 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Fy")) ")" ) ")" ))))) ; theorem :: CARD_FIN:43 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: CARD_FIN:44 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_recdef_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "Fy")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ))) ")" ) & (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XFS")))) ")" ))))) ; theorem :: CARD_FIN:45 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "Fy")) "," (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: CARD_FIN:46 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Fy")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))))))) ; theorem :: CARD_FIN:47 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "Fy")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ))) ")" )))) ; theorem :: CARD_FIN:48 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set "(" (Set (Var "Fy")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "," (Num 1) ")" ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "Fy")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: CARD_FIN:49 (Bool "for" (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X9")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set "(" ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X9")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X9")))) ")" ) ")" ))) ; theorem :: CARD_FIN:50 (Bool "for" (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X9"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X9")) ")" ) ")" ")" ) ")" ))))) ; theorem :: CARD_FIN:51 (Bool "for" (Set (Var "y")) "," (Set (Var "X9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "Ch")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "F")) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" ")" ) ($#k8_subset_1 :::"/\"::: ) (Set (Var "X9"))) ($#r1_hidden :::"="::: ) (Set ($#k2_card_fin :::"Intersection"::: ) "(" (Set "(" ($#k1_yellow20 :::"Intersect"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "X9")) ")" ) ")" ")" ) "," (Set (Var "Ch")) "," (Set (Var "y")) ")" )))) ; theorem :: CARD_FIN:52 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "G"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: CARD_FIN:53 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set "(" (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set "(" (Set (Var "Fy")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set "(" ($#k1_yellow20 :::"Intersect"::: ) "(" (Set "(" (Set (Var "Fy")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "Fy")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ")" ")" ) "," (Set (Var "k")) ")" ")" )))))))) ; theorem :: CARD_FIN:54 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: CARD_FIN:55 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" ) ")" )))) ; theorem :: CARD_FIN:56 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "XFS")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XFS"))))) "holds" (Bool (Set (Set (Var "XFS")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Fy")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XFS"))))))) ; theorem :: CARD_FIN:57 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ) ")" ))) "holds" (Bool (Set ($#k3_card_fin :::"Card_Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k24_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k6_newton :::"choose"::: ) (Set (Var "k")) ")" )))))) ; theorem :: CARD_FIN:58 (Bool "for" (Set (Var "Fy")) "being" ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Fy"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "XF")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))))) "holds" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fin :::"Choose"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_card_fin :::"Intersection"::: ) "(" (Set (Var "Fy")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "XF")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "Fy")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set (Var "XF")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k6_newton :::"choose"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ))))) ; theorem :: CARD_FIN:59 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) : (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) "}" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k6_newton :::"choose"::: ) (Set (Var "n")) ")" ) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ($#k21_binop_2 :::"-"::: ) (Set (Var "n")) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: CARD_FIN:60 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k3_stirl2_1 :::"block"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "k")) ($#k9_newton :::"!"::: ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "m")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set (Var "k")) ($#k6_newton :::"choose"::: ) (Set (Var "m")) ")" ) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k21_binop_2 :::"-"::: ) (Set (Var "m")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))) ; theorem :: CARD_FIN:61 (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "Y1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool (Set (Var "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "X1")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y1"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X1")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ")" ) ($#k9_newton :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) : (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "X1")) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) "}" )))) ; theorem :: CARD_FIN:62 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#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 (Var "X"))) & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "XF")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XF"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" ) : (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) "}" )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))))) "holds" (Bool (Set (Set (Var "XF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_newton :::"!"::: ) ")" ))) ")" ) ")" )))) ; theorem :: CARD_FIN:63 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "XF")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "XF"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) : (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" ) ")" ) "}" )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "XF"))))) "holds" (Bool (Set (Set (Var "XF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k22_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_newton :::"!"::: ) ")" ))) ")" ) ")" ))) ;