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