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:27; :: 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; :: thesis: verum