theorem Th4: :: SF_MASTR:4

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