let m be Element of NAT ; :: thesis: ( {} is_CRS_of m iff m = 0 )
set fp = <*> INT ;
thus ( {} is_CRS_of m implies m = 0 ) by Th49, CARD_1:47; :: thesis: ( m = 0 implies {} is_CRS_of m )
assume m = 0 ; :: thesis: {} is_CRS_of m
then A1: len (<*> INT ) = m ;
( {} = rng (<*> INT ) & ( for b being Nat st b in dom (<*> INT ) holds
(<*> INT ) . b in Class (Cong m),(b -' 1) ) ) ;
hence {} is_CRS_of m by A1, Def2; :: thesis: verum