let h be Integer; :: thesis: ( h <> 0 implies for n being Nat st n in dom (Sgm (PrimeDivisors>3 h)) holds
(Sgm (PrimeDivisors>3 h)) . n divides h )
set X = PrimeDivisors>3 h;
set f = Sgm (PrimeDivisors>3 h);
assume A1: h <> 0 ; :: thesis: for n being Nat st n in dom (Sgm (PrimeDivisors>3 h)) holds
(Sgm (PrimeDivisors>3 h)) . n divides h
let n be Nat; :: thesis: ( n in dom (Sgm (PrimeDivisors>3 h)) implies (Sgm (PrimeDivisors>3 h)) . n divides h )
assume n in dom (Sgm (PrimeDivisors>3 h)) ; :: thesis: (Sgm (PrimeDivisors>3 h)) . n divides h
then A2: (Sgm (PrimeDivisors>3 h)) . n in rng (Sgm (PrimeDivisors>3 h)) by FUNCT_1:def 3;
rng (Sgm (PrimeDivisors>3 h)) = PrimeDivisors>3 h by A1, FINSEQ_1:def 14;
hence (Sgm (PrimeDivisors>3 h)) . n divides h by A2, Th36; :: thesis: verum