let a, b be natural Ordinal; :: thesis: (RED a,b) *^ (a hcf b) = a
( RED a,b = a div^ (a hcf b) & a hcf b divides a ) by Def5;
hence (RED a,b) *^ (a hcf b) = a by Th11; :: thesis: verum