:: CARDFIN2  semantic presentation begin  



registrationlet "c" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k25_sin_cos :::"exp_R"::: )  "c") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registration
cluster (Set   ($#k7_power :::"number_e"::: )  ) ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; 
theorem :: CARDFIN2:1 (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )) "is"   ($#v2_abian :::"without_fixpoints"::: )  ) ; 
 
theorem :: CARDFIN2:2 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k25_sin_cos :::"exp_R"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 begin  definitionlet "n" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"round"::: "n" ->   ($#m1_hidden :::"Integer":::) equals :: CARDFIN2:def 1 (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" "n"  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ); end; 





:: deftheorem    defines :::"round"::: CARDFIN2:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_cardfin2 :::"round"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "n"))  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))); 
 
theorem :: CARDFIN2:3 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_cardfin2 :::"round"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: CARDFIN2:4 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "a"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "b")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2)))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cardfin2 :::"round"::: )  (Set (Var "b")))))) ; 
 begin  
theorem :: CARDFIN2:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set   ($#k25_sin_cos :::"exp_R"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k6_taylor_1 :::"Taylor"::: )   "(" (Set  ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k25_sin_cos :::"exp_R"::: )  (Set (Var "c")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k10_binop_2 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k3_newton :::"!"::: )  ")" ) ")" )))  ")" )))) ; 
 
theorem :: CARDFIN2:6 (Bool  "for" (Set (Var "n")) "being"   ($#v2_xxreal_0 :::"positive"::: )    ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k7_binop_2 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k3_newton :::"!"::: )  ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k25_sin_cos :::"exp_R"::: )  (Set (Var "c")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k19_binop_2 :::"-"::: )  (Num 1) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k3_newton :::"!"::: )  ")" ) ")" ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2))))) ; 
 definitionlet "s" be    ($#m1_hidden :::"set"::: )  ; func  :::"derangements"::: "s" ->    ($#m1_hidden :::"set"::: )   equals :: CARDFIN2:def 2  "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Permutation":::) "of" "s" : (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"derangements"::: CARDFIN2:def 2 :  (Bool  "for" (Set (Var "s")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "s")) : (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )  "}"  )); 
 registrationlet "s" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_cardfin2 :::"derangements"::: )  "s") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CARDFIN2:7 (Bool  "for" (Set (Var "s")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "h")) where h "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "s")) "," (Set (Var "s")) : (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 "s")))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))  ")" )  ")" )  "}"  )) ; 
 
theorem :: CARDFIN2:8 (Bool  "for" (Set (Var "s")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k19_binop_2 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")) ")" ) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k3_newton :::"!"::: )  ")" )  ($#k12_binop_2 :::"/"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_binop_2 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k3_newton :::"!"::: )  ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k25_sin_cos :::"exp_R"::: )  (Set (Var "c")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k19_binop_2 :::"-"::: )  (Num 1) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k3_newton :::"!"::: )  ")" ) ")" ) ")" )))  ")" ))) ; 
 
theorem :: CARDFIN2:9 (Bool  "for" (Set (Var "s")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "holds" (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")) ")" ) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k3_newton :::"!"::: )  ")" )  ($#k12_binop_2 :::"/"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2)))) ; 
 
theorem :: CARDFIN2:10 (Bool  "for" (Set (Var "s")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cardfin2 :::"round"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" )  ($#k3_newton :::"!"::: )  ")" )  ($#k12_binop_2 :::"/"::: )  (Set  ($#k8_power :::"number_e"::: ) ) ")" )))) ; 
 
theorem :: CARDFIN2:11 (Bool (Set   ($#k2_cardfin2 :::"derangements"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: CARDFIN2:12 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_cardfin2 :::"derangements"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 definitionfunc  :::"der_seq":::  ->   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k4_numbers :::"INT"::: ) ) means :: CARDFIN2:def 3 (Bool  "("  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k22_binop_2 :::"*"::: )  (Set  "(" (Set  "(" it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "(" it  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))  ")" )  ")" ); end; 




:: deftheorem    defines :::"der_seq"::: CARDFIN2:def 3 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k4_numbers :::"INT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_cardfin2 :::"der_seq"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k22_binop_2 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "(" (Set (Var "b1"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))  ")" )  ")" )  ")" )); 
 registrationlet "c" be   ($#m1_hidden :::"Integer":::); let "F" be   ($#m1_hidden :::"XFinSequence":::) "of" ; 
cluster (Set "c"  ($#k24_valued_1 :::"(#)"::: )  "F") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )   (Set   ($#k4_numbers :::"INT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "F" be   ($#v1_xboole_0 :::"empty"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "c"  ($#k24_valued_1 :::"(#)"::: )  "F") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: CARDFIN2:13 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "c"))  ($#k22_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "F")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "F")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k22_binop_2 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "F")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" ))))) ; 
 
theorem :: CARDFIN2:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "X")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "N"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c"))  ($#k22_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "X")) ")" ) ")" )  ($#k20_binop_2 :::"+"::: )  (Set  "(" (Set (Var "N"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "X")) ")" ) ")" ))))) ; 
 
theorem :: CARDFIN2:15 (Bool  "for" (Set (Var "s")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k3_cardfin2 :::"der_seq"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_cardfin2 :::"derangements"::: )  (Set (Var "s")) ")" )))) ; 
 begin  definitionlet "s", "t" be    ($#m1_hidden :::"set"::: )  ; func  :::"not-one-to-one":::  "(" "s" "," "t" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" "s" "," "t" ")"  ")" ) equals :: CARDFIN2:def 4  "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" "s" "," "t" : (Bool (Bool  "not" (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))  "}"  ; end; 






:: deftheorem    defines :::"not-one-to-one"::: CARDFIN2:def 4 :  (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_cardfin2 :::"not-one-to-one"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "s")) "," (Set (Var "t")) : (Bool (Bool  "not" (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))  "}"  )); 
 registrationlet "s", "t" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_cardfin2 :::"not-one-to-one"::: )   "(" "s" "," "t" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; scheme  :: CARDFIN2:sch 1 FraenkelDiff{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) : (Bool P1[(Set (Var "f"))])  "}"    ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) ")"  ")" )  ($#k6_subset_1 :::"\"::: )   "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) : (Bool P1[(Set (Var "f"))])  "}"  ))
 provided
 "("  (Bool (Bool (Set F2 "("  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set F1 "("  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" 
 proof 


end; 
theorem :: CARDFIN2:16 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "s")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "t"))))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k4_cardfin2 :::"not-one-to-one"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "t")) ")" )  ($#k13_newton :::"|^"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" ) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "t")) ")" )  ($#k3_newton :::"!"::: )  ")" )  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "t")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "s")) ")" ) ")" )  ($#k3_newton :::"!"::: )  ")" ) ")" )))) ; 
 
theorem :: CARDFIN2:17 (Bool  "for" (Set (Var "s")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "t")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Num 23)) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Num 365))) "holds"  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k4_cardfin2 :::"not-one-to-one"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" ))))) ; 
 
theorem :: CARDFIN2:18 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Num 23)) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Num 365))) "holds"  (Bool (Set   ($#k1_rpr_1 :::"prob"::: )  (Set  "("  ($#k4_cardfin2 :::"not-one-to-one"::: )   "(" (Set (Var "s")) "," (Set (Var "t")) ")"  ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2)))) ;