let s, t be non zero Nat; :: thesis: ( s,t are_coprime implies dom (Euler_factorization s) misses dom (Euler_factorization t) )
A1: dom (Euler_factorization s) = support (ppf s) by Def1;
A2: dom (Euler_factorization t) = support (ppf t) by Def1;
A3: support (ppf s) = support (pfexp s) by NAT_3:def 9;
support (ppf t) = support (pfexp t) by NAT_3:def 9;
hence ( s,t are_coprime implies dom (Euler_factorization s) misses dom (Euler_factorization t) ) by A1, A2, A3, NAT_3:44; :: thesis: verum