let h be Integer; :: thesis: ( h <> 0 implies rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) c= SetPrimes )
set X = PrimeDivisors>3 h;
set F = Sgm (PrimeDivisors>3 h);
set f = <*2,3*>;
assume A1: h <> 0 ; :: thesis: rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) c= SetPrimes
A2: rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) = (rng <*2,3*>) \/ (rng (Sgm (PrimeDivisors>3 h))) by FINSEQ_1:31;
A3: rng <*2,3*> c= SetPrimes

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*2,3*> or x in SetPrimes )
assume x in rng <*2,3*> ; :: thesis: x in SetPrimes
then x in {2,3} by FINSEQ_2:127;
then ( x = 2 or x = 3 ) by TARSKI:def 2;
hence x in SetPrimes by NEWTON:def 6, XPRIMES1:2, XPRIMES1:3; :: thesis: verum

end;

rng (Sgm (PrimeDivisors>3 h)) c= SetPrimes

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Sgm (PrimeDivisors>3 h)) or x in SetPrimes )
assume x in rng (Sgm (PrimeDivisors>3 h)) ; :: thesis: x in SetPrimes
then x in PrimeDivisors>3 h by A1, FINSEQ_1:def 14;
then x is prime Nat by Th37;
hence x in SetPrimes by NEWTON:def 6; :: thesis: verum

end;

hence rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) c= SetPrimes by A2, A3, XBOOLE_1:8; :: thesis: verum