theorem Th32: :: AFINSQ_2:32

for X, Y being finite natural-membered set st Y <> {} & X <N< Y holds
(Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X))