theorem Th3: :: SF_MASTR:3

for a1, a2, b1, b2 being Int-Location st SubFrom (a1,b1) = SubFrom (a2,b2) holds
( a1 = a2 & b1 = b2 )