let l, i, j, k be natural Ordinal; :: thesis: (i / j) *' (k / l) = (i *^ k) / (j *^ l)

per cases ( ( j <> {} & l <> {} ) or j = {} or l = {} ) ;

suppose A1: ( j <> {} & l <> {} ) ; :: thesis: (i / j) *' (k / l) = (i *^ k) / (j *^ l)

then A2: ( denominator (k / l) = RED l,k & denominator (i / j) = RED j,i ) by Th48;
( numerator (k / l) = RED k,l & numerator (i / j) = RED i,j ) by A1, Th48;
hence (i / j) *' (k / l) = (((RED i,j) *^ (RED k,l)) *^ (i hcf j)) / (((RED j,i) *^ (RED l,k)) *^ (i hcf j)) by A1, A2, Th20, Th50
.= ((RED k,l) *^ ((RED i,j) *^ (i hcf j))) / (((RED j,i) *^ (RED l,k)) *^ (i hcf j)) by ORDINAL3:58
.= ((RED k,l) *^ i) / (((RED j,i) *^ (RED l,k)) *^ (i hcf j)) by Th26
.= ((RED k,l) *^ i) / ((RED l,k) *^ ((RED j,i) *^ (i hcf j))) by ORDINAL3:58
.= ((RED k,l) *^ i) / ((RED l,k) *^ j) by Th26
.= (((RED k,l) *^ i) *^ (l hcf k)) / (((RED l,k) *^ j) *^ (l hcf k)) by A1, Th20, Th50
.= (i *^ ((RED k,l) *^ (l hcf k))) / (((RED l,k) *^ j) *^ (l hcf k)) by ORDINAL3:58
.= (i *^ k) / (((RED l,k) *^ j) *^ (l hcf k)) by Th26
.= (i *^ k) / (j *^ ((RED l,k) *^ (l hcf k))) by ORDINAL3:58
.= (i *^ k) / (j *^ l) by Th26 ;
:: thesis: verum

end;

suppose A3: ( j = {} or l = {} ) ; :: thesis: (i / j) *' (k / l) = (i *^ k) / (j *^ l)

then ( i / j = {} or k / l = {} ) by Def10;
then A4: (i / j) *' (k / l) = {} by Th54;
j *^ l = {} by A3, ORDINAL2:52;
hence (i / j) *' (k / l) = (i *^ k) / (j *^ l) by A4, Def10; :: thesis: verum

end;

end;