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

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