let a, b, c be natural Ordinal; :: thesis: ( c <> {} implies RED ((a *^ c),(b *^ c)) = RED (a,b) )
assume A1: c <> {} ; :: thesis: RED ((a *^ c),(b *^ c)) = RED (a,b)
( a <> {} implies a hcf b <> {} ) by Th18;
then A2: ( a <> {} implies (a hcf b) *^ c <> {} ) by A1, ORDINAL3:31;
A3: ( RED ({},b) = {} & {} *^ ((a hcf b) *^ c) = {} ) by ORDINAL2:35, ORDINAL3:70;
A4: a hcf b divides a by Def5;
thus RED ((a *^ c),(b *^ c)) = (a *^ c) div^ ((a hcf b) *^ c) by Th17
.= (((a div^ (a hcf b)) *^ (a hcf b)) *^ c) div^ ((a hcf b) *^ c) by A4, Th7
.= ((RED (a,b)) *^ ((a hcf b) *^ c)) div^ ((a hcf b) *^ c) by ORDINAL3:50
.= RED (a,b) by A2, A3, ORDINAL3:68, ORDINAL3:70 ; :: thesis: verum