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: x = (numerator x) / (denominator x) by Th39;
z = (numerator z) / (denominator z) by Th39;
hence (x *' y) *' z = (((numerator x) *^ (numerator y)) *^ (numerator z)) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by Th49
.= ((numerator x) *^ ((numerator y) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:50
.= ((numerator x) *^ ((numerator y) *^ (numerator z))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:50
.= x *' (y *' z) by A1, Th49 ;
:: thesis: verum