let l, j, i, k be natural Ordinal; ( j <> {} & l <> {} implies (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l) )
assume that
A1:
j <> {}
and
A2:
l <> {}
; (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l)
A3:
( denominator (k / l) = RED l,k & denominator (i / j) = RED j,i )
by A1, A2, Th48;
( numerator (k / l) = RED k,l & numerator (i / j) = RED i,j )
by A1, A2, 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, A3, 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 A2, 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
;
verum