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 Th42;
( numerator (k / l) = RED (k,l) & numerator (i / j) = RED (i,j) ) by A1, Th42;
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, Th15, Th44
.= ((RED (k,l)) *^ ((RED (i,j)) *^ (i hcf j))) / (((RED (j,i)) *^ (RED (l,k))) *^ (i hcf j)) by ORDINAL3:50
.= ((RED (k,l)) *^ i) / (((RED (j,i)) *^ (RED (l,k))) *^ (i hcf j)) by Th21
.= ((RED (k,l)) *^ i) / ((RED (l,k)) *^ ((RED (j,i)) *^ (i hcf j))) by ORDINAL3:50
.= ((RED (k,l)) *^ i) / ((RED (l,k)) *^ j) by Th21
.= (((RED (k,l)) *^ i) *^ (l hcf k)) / (((RED (l,k)) *^ j) *^ (l hcf k)) by A1, Th15, Th44
.= (i *^ ((RED (k,l)) *^ (l hcf k))) / (((RED (l,k)) *^ j) *^ (l hcf k)) by ORDINAL3:50
.= (i *^ k) / (((RED (l,k)) *^ j) *^ (l hcf k)) by Th21
.= (i *^ k) / (j *^ ((RED (l,k)) *^ (l hcf k))) by ORDINAL3:50
.= (i *^ k) / (j *^ l) by Th21 ;
:: 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 Th48;
j *^ l = {} by A3, ORDINAL2:35;
hence (i / j) *' (k / l) = (i *^ k) / (j *^ l) by A4, Def10; :: thesis: verum
end;
end;