let a, b, c be natural Ordinal; ( c <> {} implies (a *^ c) / (b *^ c) = a / b )
assume A1:
c <> {}
; (a *^ c) / (b *^ c) = a / b
per cases
( b = {} or b <> {} )
;
suppose A2:
b <> {}
;
(a *^ c) / (b *^ c) = a / bthen A3:
b *^ c <> {}
by A1, ORDINAL3:31;
then A4:
denominator ((a *^ c) / (b *^ c)) =
RED (
(b *^ c),
(a *^ c))
by Th42
.=
RED (
b,
a)
by A1, Th28
.=
denominator (a / b)
by A2, Th42
;
numerator ((a *^ c) / (b *^ c)) =
RED (
(a *^ c),
(b *^ c))
by A3, Th42
.=
RED (
a,
b)
by A1, Th28
.=
numerator (a / b)
by A2, Th42
;
hence (a *^ c) / (b *^ c) =
(numerator (a / b)) / (denominator (a / b))
by A4, Th39
.=
a / b
by Th39
;
verum end; end;