let l, j, i, 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, Th48;
set nx = numerator (i / j);
set dx = denominator (i / j);
A4: denominator (i / j) = RED (j,i) by A1, Th48;
A5: denominator (k / l) = RED (l,k) by A2, Th48;
A6: numerator (i / j) = RED (i,j) by A1, Th48;

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, Th26;
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, Th26
.= j *^ ((numerator (k / l)) *^ (l hcf k)) by ORDINAL3:50
.= j *^ k by A3, Th26 ;
:: 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, Th33;
then A8: denominator (i / j) = denominator (k / l) by A1, A5, Th33;
numerator (i / j) = RED ((j *^ k),(j *^ l)) by A2, A6, A7, Th33;
then numerator (i / j) = numerator (k / l) by A1, A3, Th33;
then i / j = (numerator (k / l)) / (denominator (k / l)) by A8, Th45;
hence i / j = k / l by Th45; :: thesis: verum