theorem Th11: :: SF_MASTR:11

for a1, a2 being Int-Location
for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds
( a1 = a2 & f1 = f2 )