theorem :: MATRTOP1:13

for X being set
for f1, f2, g1, g2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds
Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))