let l, j, i, k be natural Ordinal; :: thesis: ( j <> {} & l <> {} implies ( i / j = k / l iff i *^ l = j *^ k ) )
assume A1: ( j <> {} & l <> {} ) ; :: thesis: ( i / j = k / l iff i *^ l = j *^ k )
set x = i / j;
set y = k / l;
set nx = numerator (i / j);
set dx = denominator (i / j);
set ny = numerator (k / l);
set dy = denominator (k / l);
A2: ( numerator (i / j) = RED i,j & denominator (i / j) = RED j,i ) by A1, Th48;
A3: ( numerator (k / l) = RED k,l & denominator (k / l) = RED l,k ) 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 A2, A3, Th26;
hence i *^ l = (((numerator (k / l)) *^ (i hcf j)) *^ (denominator (i / j))) *^ (l hcf k) by ORDINAL3:58
.= ((numerator (k / l)) *^ ((i hcf j) *^ (denominator (i / j)))) *^ (l hcf k) by ORDINAL3:58
.= ((numerator (k / l)) *^ j) *^ (l hcf k) by A2, Th26
.= j *^ ((numerator (k / l)) *^ (l hcf k)) by ORDINAL3:58
.= j *^ k by A3, Th26 ;
:: thesis: verum

end;

assume i *^ l = j *^ k ; :: thesis: i / j = k / l
then ( numerator (i / j) = RED (j *^ k),(j *^ l) & denominator (i / j) = RED (j *^ l),(j *^ k) ) by A1, A2, Th33;
then ( numerator (i / j) = numerator (k / l) & denominator (i / j) = denominator (k / l) ) by A1, A3, Th33;
then i / j = (numerator (k / l)) / (denominator (k / l)) by Th45;
hence i / j = k / l by Th45; :: thesis: verum