theorem Th3: :: FINSEQ_6:129

for X, Y being set
for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds
(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))