let s, t be finite set ; :: thesis: ( card s <= card t implies card (not-one-to-one s,t) = ((card t) |^ (card s)) - (((card t) ! ) / (((card t) -' (card s)) ! )) )
assume A: card s <= card t ; :: thesis: card (not-one-to-one s,t) = ((card t) |^ (card s)) - (((card t) ! ) / (((card t) -' (card s)) ! ))
defpred S₁[ Function] means $1 is one-to-one ;
set onetoone = { f where f is Function of s,t : f is one-to-one } ;
Z0: ( t = {} implies s = {} )

proof

assume t = {} ; :: thesis: s = {}
then card t = 0 ;
hence s = {} by A; :: thesis: verum

end;

{ f where f is Function of s,t : f is one-to-one } c= Funcs s,t

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of s,t : f is one-to-one } or x in Funcs s,t )
assume x in { f where f is Function of s,t : f is one-to-one } ; :: thesis: x in Funcs s,t
then ex f being Function of s,t st
( x = f & f is one-to-one ) ;
hence x in Funcs s,t by Z0, FUNCT_2:11; :: thesis: verum

end;

then reconsider onetoone = { f where f is Function of s,t : f is one-to-one } as Subset of (Funcs s,t) ;
{ f where f is Function of s,t : not S₁[f] } = (Funcs s,t) \ { f where f is Function of s,t : S₁[f] } from CARDFIN2:sch 1(Z0);
then card (not-one-to-one s,t) = (card (Funcs s,t)) - (card onetoone) by CARD_2:63
.= (card (Funcs s,t)) - (((card t) ! ) / (((card t) -' (card s)) ! )) by CARD_FIN:7, A
.= ((card t) |^ (card s)) - (((card t) ! ) / (((card t) -' (card s)) ! )) by CARD_FIN:4, Z0 ;
hence card (not-one-to-one s,t) = ((card t) |^ (card s)) - (((card t) ! ) / (((card t) -' (card s)) ! )) ; :: thesis: verum