let x, y, z be Element of RAT+ ; :: thesis: (x + y) + z = x + (y + z)
set nx = numerator x;
set ny = numerator y;
set nz = numerator z;
set dx = denominator x;
set dy = denominator y;
set dz = denominator z;
A1: ( denominator x <> {} & denominator y <> {} & denominator z <> {} ) by Th41;
then A2: ( (denominator x) *^ (denominator y) <> {} & (denominator y) *^ (denominator z) <> {} ) by ORDINAL3:34;
thus (x + y) + z = ((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) / ((denominator x) *^ (denominator y))) + ((numerator z) / (denominator z)) by Th45
.= (((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) *^ (denominator z)) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by A1, A2, Th52
.= (((((numerator x) *^ (denominator y)) *^ (denominator z)) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:54
.= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:58
.= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:58
.= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z)))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:58
.= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ ((numerator y) *^ (denominator z))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:33
.= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:54
.= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:58
.= ((((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))) / ((denominator y) *^ (denominator z))) + ((numerator x) / (denominator x)) by A1, A2, Th52
.= x + (y + z) by Th45 ; :: thesis: verum