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 A1: 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 } ;
A2: ( t = {} implies s = {} ) by A1;
{ f where f is Function of s,t : f is one-to-one } c= Funcs (s,t)

proof

let x be object ; :: 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 A2, FUNCT_2:8; :: 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(A2);
then card (not-one-to-one (s,t)) = (card (Funcs (s,t))) - (card onetoone) by CARD_2:44
.= (card (Funcs (s,t))) - (((card t) !) / (((card t) -' (card s)) !)) by A1, CARD_FIN:7
.= ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) by A2, CARD_FIN:4 ;
hence card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) ; :: thesis: verum