let l, i, j, 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, Th42;
( numerator (k / l) = RED (k,l) & numerator (i / j) = RED (i,j) )
by A1, A2, Th42;
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, Th15, Th44
.=
((((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:50
.=
((((RED (i,j)) *^ (RED (l,k))) +^ ((RED (j,i)) *^ (RED (k,l)))) *^ (i hcf j)) / ((RED (l,k)) *^ j)
by Th21
.=
((((RED (i,j)) *^ (RED (l,k))) *^ (i hcf j)) +^ (((RED (j,i)) *^ (RED (k,l))) *^ (i hcf j))) / ((RED (l,k)) *^ j)
by ORDINAL3:46
.=
(((RED (l,k)) *^ ((RED (i,j)) *^ (i hcf j))) +^ (((RED (j,i)) *^ (RED (k,l))) *^ (i hcf j))) / ((RED (l,k)) *^ j)
by ORDINAL3:50
.=
(((RED (l,k)) *^ i) +^ (((RED (j,i)) *^ (RED (k,l))) *^ (i hcf j))) / ((RED (l,k)) *^ j)
by Th21
.=
(((RED (l,k)) *^ i) +^ ((RED (k,l)) *^ ((RED (j,i)) *^ (i hcf j)))) / ((RED (l,k)) *^ j)
by ORDINAL3:50
.=
(((RED (l,k)) *^ i) +^ ((RED (k,l)) *^ j)) / ((RED (l,k)) *^ j)
by Th21
.=
((((RED (l,k)) *^ i) +^ ((RED (k,l)) *^ j)) *^ (k hcf l)) / (((RED (l,k)) *^ j) *^ (k hcf l))
by A2, Th15, Th44
.=
((((RED (l,k)) *^ i) +^ ((RED (k,l)) *^ j)) *^ (k hcf l)) / (j *^ ((RED (l,k)) *^ (k hcf l)))
by ORDINAL3:50
.=
((((RED (l,k)) *^ i) +^ ((RED (k,l)) *^ j)) *^ (k hcf l)) / (j *^ l)
by Th21
.=
((((RED (l,k)) *^ i) *^ (k hcf l)) +^ (((RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)
by ORDINAL3:46
.=
((i *^ ((RED (l,k)) *^ (k hcf l))) +^ (((RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)
by ORDINAL3:50
.=
((i *^ l) +^ (((RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)
by Th21
.=
((i *^ l) +^ (j *^ ((RED (k,l)) *^ (k hcf l)))) / (j *^ l)
by ORDINAL3:50
.=
((i *^ l) +^ (j *^ k)) / (j *^ l)
by Th21
;
verum