let h, s be non zero Nat; :: thesis: ( ( for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ) implies support (prime_factorization s) c= support (prime_factorization h) )
assume A1: for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ; :: thesis: support (prime_factorization s) c= support (prime_factorization h)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (prime_factorization s) or x in support (prime_factorization h) )
assume A2: x in support (prime_factorization s) ; :: thesis: x in support (prime_factorization h)
then reconsider q = x as Prime by NEWTON:def 6;
q divides h by Th5, A2, A1;
then q in support (pfexp h) by ORDINAL1:def 13, NAT_3:37;
hence x in support (prime_factorization h) by NAT_3:def 9; :: thesis: verum