let l, j, i, k be natural Ordinal; :: thesis: ( j <> {} & l <> {} implies (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l) )
assume A1: ( j <> {} & l <> {} ) ; :: thesis: (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l)
then ( numerator (k / l) = RED k,l & numerator (i / j) = RED i,j & denominator (k / l) = RED l,k & denominator (i / j) = RED j,i ) by Th48;
hence (i / j) + (k / l) = ((((RED i,j) *^ (RED l,k)) +^ ((RED j,i) *^ (RED k,l))) *^ (i hcf j)) / (((RED j,i) *^ (RED l,k)) *^ (i hcf j)) by A1, Th20, Th50
.= ((((RED i,j) *^ (RED l,k)) +^ ((RED j,i) *^ (RED k,l))) *^ (i hcf j)) / ((RED l,k) *^ ((RED j,i) *^ (i hcf j))) by ORDINAL3:58
.= ((((RED i,j) *^ (RED l,k)) +^ ((RED j,i) *^ (RED k,l))) *^ (i hcf j)) / ((RED l,k) *^ j) by Th26
.= ((((RED i,j) *^ (RED l,k)) *^ (i hcf j)) +^ (((RED j,i) *^ (RED k,l)) *^ (i hcf j))) / ((RED l,k) *^ j) by ORDINAL3:54
.= (((RED l,k) *^ ((RED i,j) *^ (i hcf j))) +^ (((RED j,i) *^ (RED k,l)) *^ (i hcf j))) / ((RED l,k) *^ j) by ORDINAL3:58
.= (((RED l,k) *^ i) +^ (((RED j,i) *^ (RED k,l)) *^ (i hcf j))) / ((RED l,k) *^ j) by Th26
.= (((RED l,k) *^ i) +^ ((RED k,l) *^ ((RED j,i) *^ (i hcf j)))) / ((RED l,k) *^ j) by ORDINAL3:58
.= (((RED l,k) *^ i) +^ ((RED k,l) *^ j)) / ((RED l,k) *^ j) by Th26
.= ((((RED l,k) *^ i) +^ ((RED k,l) *^ j)) *^ (k hcf l)) / (((RED l,k) *^ j) *^ (k hcf l)) by A1, Th20, Th50
.= ((((RED l,k) *^ i) +^ ((RED k,l) *^ j)) *^ (k hcf l)) / (j *^ ((RED l,k) *^ (k hcf l))) by ORDINAL3:58
.= ((((RED l,k) *^ i) +^ ((RED k,l) *^ j)) *^ (k hcf l)) / (j *^ l) by Th26
.= ((((RED l,k) *^ i) *^ (k hcf l)) +^ (((RED k,l) *^ j) *^ (k hcf l))) / (j *^ l) by ORDINAL3:54
.= ((i *^ ((RED l,k) *^ (k hcf l))) +^ (((RED k,l) *^ j) *^ (k hcf l))) / (j *^ l) by ORDINAL3:58
.= ((i *^ l) +^ (((RED k,l) *^ j) *^ (k hcf l))) / (j *^ l) by Th26
.= ((i *^ l) +^ (j *^ ((RED k,l) *^ (k hcf l)))) / (j *^ l) by ORDINAL3:58
.= ((i *^ l) +^ (j *^ k)) / (j *^ l) by Th26 ;
:: thesis: verum