let m be Nat; :: thesis: RelPrimes m is_RRS_of m
A1: RelPrimes m c= Seg m by Th1;
A2: ( rng (Sgm (RelPrimes m)) = RelPrimes m & len (Sgm (RelPrimes m)) = len (Sgm (RelPrimes m)) ) by A1, FINSEQ_1:def 13;
rng (Sgm (RelPrimes m)) c= INT ;
then A3: Sgm (RelPrimes m) is FinSequence of INT by FINSEQ_1:def 4;
for a being Nat st a in dom (Sgm (RelPrimes m)) holds
(Sgm (RelPrimes m)) . a in Class ((Cong m),((Sgm (RelPrimes m)) . a))
proof
let a be Nat; :: thesis: ( a in dom (Sgm (RelPrimes m)) implies (Sgm (RelPrimes m)) . a in Class ((Cong m),((Sgm (RelPrimes m)) . a)) )
assume a in dom (Sgm (RelPrimes m)) ; :: thesis: (Sgm (RelPrimes m)) . a in Class ((Cong m),((Sgm (RelPrimes m)) . a))
(Sgm (RelPrimes m)) . a,(Sgm (RelPrimes m)) . a are_congruent_mod m by INT_1:11;
then [((Sgm (RelPrimes m)) . a),((Sgm (RelPrimes m)) . a)] in Cong m by INT_4:def 1;
hence (Sgm (RelPrimes m)) . a in Class ((Cong m),((Sgm (RelPrimes m)) . a)) by EQREL_1:18; :: thesis: verum
end;
then for d being Element of NAT st d in dom (Sgm (RelPrimes m)) holds
(Sgm (RelPrimes m)) . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) ;
hence RelPrimes m is_RRS_of m by A2, A3; :: thesis: verum