theorem Th45: :: ARYTM_3:45

for l, i, j, k being natural Ordinal st j <> {} & l <> {} holds
( i / j = k / l iff i *^ l = j *^ k )