let l, i, j, k be natural Ordinal; :: thesis: ( j <> {} & l <> {} implies ( i / j = k / l iff i *^ l = j *^ k ) )
assume that
A1: j <> {} and
A2: l <> {} ; :: thesis: ( i / j = k / l iff i *^ l = j *^ k )
set x = i / j;
set y = k / l;
set ny = numerator (k / l);
set dy = denominator (k / l);
A3: numerator (k / l) = RED (k,l) by A2, Th42;
set nx = numerator (i / j);
set dx = denominator (i / j);
A4: denominator (i / j) = RED (j,i) by A1, Th42;
A5: denominator (k / l) = RED (l,k) by A2, Th42;
A6: numerator (i / j) = RED (i,j) by A1, Th42;

hereby :: thesis: ( i *^ l = j *^ k implies i / j = k / l )

assume i / j = k / l ; :: thesis: i *^ l = j *^ k
then ( i = (numerator (k / l)) *^ (i hcf j) & l = (denominator (i / j)) *^ (l hcf k) ) by A6, A5, Th21;
hence i *^ l = (((numerator (k / l)) *^ (i hcf j)) *^ (denominator (i / j))) *^ (l hcf k) by ORDINAL3:50
.= ((numerator (k / l)) *^ ((i hcf j) *^ (denominator (i / j)))) *^ (l hcf k) by ORDINAL3:50
.= ((numerator (k / l)) *^ j) *^ (l hcf k) by A4, Th21
.= j *^ ((numerator (k / l)) *^ (l hcf k)) by ORDINAL3:50
.= j *^ k by A3, Th21 ;
:: thesis: verum

end;

assume A7: i *^ l = j *^ k ; :: thesis: i / j = k / l
then denominator (i / j) = RED ((j *^ l),(j *^ k)) by A2, A4, Th28;
then A8: denominator (i / j) = denominator (k / l) by A1, A5, Th28;
numerator (i / j) = RED ((j *^ k),(j *^ l)) by A2, A6, A7, Th28;
then numerator (i / j) = numerator (k / l) by A1, A3, Th28;
then i / j = (numerator (k / l)) / (denominator (k / l)) by A8, Th39;
hence i / j = k / l by Th39; :: thesis: verum