let r, s, t be Element of RAT+ ; ( s + t = r + t implies s = r )
assume A1:
s + t = r + t
; s = r
set r1 = numerator r;
set r2 = denominator r;
set t1 = numerator t;
set t2 = denominator t;
set s1 = numerator s;
set s2 = denominator s;
A2:
denominator t <> {}
by Th35;
A3:
denominator s <> {}
by Th35;
then A4:
(denominator s) *^ (denominator t) <> {}
by A2, ORDINAL3:31;
A5:
denominator r <> {}
by Th35;
then
(denominator r) *^ (denominator t) <> {}
by A2, ORDINAL3:31;
then (((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ ((denominator r) *^ (denominator t)) =
(((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ ((denominator s) *^ (denominator t))
by A1, A4, Th45
.=
((((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s)) *^ (denominator t)
by ORDINAL3:50
;
then
((((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ (denominator r)) *^ (denominator t) = ((((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s)) *^ (denominator t)
by ORDINAL3:50;
then (((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ (denominator r) =
(((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s)
by A2, ORDINAL3:33
.=
(((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator r) *^ (numerator t)) *^ (denominator s))
by ORDINAL3:46
;
then (((numerator s) *^ (denominator t)) *^ (denominator r)) +^ (((denominator s) *^ (numerator t)) *^ (denominator r)) =
(((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator r) *^ (numerator t)) *^ (denominator s))
by ORDINAL3:46
.=
(((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator s) *^ (numerator t)) *^ (denominator r))
by ORDINAL3:50
;
then ((numerator s) *^ (denominator t)) *^ (denominator r) =
((numerator r) *^ (denominator t)) *^ (denominator s)
by ORDINAL3:21
.=
((numerator r) *^ (denominator s)) *^ (denominator t)
by ORDINAL3:50
;
then
((numerator s) *^ (denominator r)) *^ (denominator t) = ((numerator r) *^ (denominator s)) *^ (denominator t)
by ORDINAL3:50;
then
(numerator s) *^ (denominator r) = (numerator r) *^ (denominator s)
by A2, ORDINAL3:33;
then (numerator s) / (denominator s) =
(numerator r) / (denominator r)
by A3, A5, Th45
.=
r
by Th39
;
hence
s = r
by Th39; verum