let l, i, j, k be natural Ordinal; ( j <> {} & l <> {} implies ( i / j = k / l iff i *^ l = j *^ k ) )
assume that
A1:
j <> {}
and
A2:
l <> {}
; ( 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 ( i *^ l = j *^ k implies i / j = k / l )
end;
assume A7:
i *^ l = j *^ k
; 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; verum