theorem Th31: :: AFINSQ_2:31

for i being Nat
for X, Y being finite natural-membered set st X <N< Y & i < len (Sgm0 Y) holds
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))