let m be Nat; :: thesis: ( {} is_RRS_of m iff m = 0 )
thus ( {} is_RRS_of m implies m = 0 ) :: thesis: ( m = 0 implies {} is_RRS_of m )
proof
assume {} is_RRS_of m ; :: thesis: m = 0
then Euler m = card {} by Th24;
hence m = 0 by PEPIN:42; :: thesis: verum
end;
assume A1: m = 0 ; :: thesis: {} is_RRS_of m
reconsider fp = <*> INT as FinSequence of INT ;
RelPrimes m c= Seg m by Th1;
then card (RelPrimes m) <= card (Seg m) by NAT_1:43;
then card (RelPrimes m) <= 0 by A1;
then card (RelPrimes m) = 0 ;
then A2: len (Sgm (RelPrimes m)) = len fp by Lm3, FINSEQ_3:43;
for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) ;
hence {} is_RRS_of m by RELAT_1:38, A2; :: thesis: verum