let a be Nat; :: thesis: for X being included_in_Seg set st a in X holds
a divides Product (Sgm X)
let X be included_in_Seg set ; :: thesis: ( a in X implies a divides Product (Sgm X) )
rng (Sgm X) = X by FINSEQ_1:def 14;
hence ( a in X implies a divides Product (Sgm X) ) by NAT_3:7; :: thesis: verum