for X being set
for P being finite without_zero Subset of NAT st X c= P holds
Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))