let c, a, b 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 Th23;
then A2: ( a <> {} implies (a hcf b) *^ c <> {} ) by A1, ORDINAL3:34;
A3: ( RED {} ,b = {} & {} *^ ((a hcf b) *^ c) = {} ) by ORDINAL2:52, ORDINAL3:83;
A4: a hcf b divides a by Def5;
thus RED (a *^ c),(b *^ c) = (a *^ c) div^ ((a hcf b) *^ c) by Th22
.= (((a div^ (a hcf b)) *^ (a hcf b)) *^ c) div^ ((a hcf b) *^ c) by A4, Th11
.= ((RED a,b) *^ ((a hcf b) *^ c)) div^ ((a hcf b) *^ c) by ORDINAL3:58
.= RED a,b by A2, A3, ORDINAL3:81, ORDINAL3:83 ; :: thesis: verum