let a, c, b be natural Ordinal; :: thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

per cases ( c = {} or ( c <> {} & a <> {} ) or a = {} ) ;

suppose c = {} ; :: thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

then ( a *^ c = {} & b *^ c = {} & (a hcf b) *^ c = {} ) by ORDINAL2:52;
hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by Th21; :: thesis: verum

end;

suppose A1: ( c <> {} & a <> {} ) ; :: thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

reconsider d = (a hcf b) *^ c as Element of omega by ORDINAL1:def 13;
set e = ((a *^ c) hcf (b *^ c)) div^ d;
( a hcf b divides a & a hcf b divides b ) by Def5;
then ( a = (a hcf b) *^ (a div^ (a hcf b)) & b = (a hcf b) *^ (b div^ (a hcf b)) ) by Th11;
then ( a *^ c = d *^ (a div^ (a hcf b)) & b *^ c = d *^ (b div^ (a hcf b)) ) by ORDINAL3:58;
then ( d divides a *^ c & d divides b *^ c ) by Def3;
then d divides (a *^ c) hcf (b *^ c) by Def5;
then A2: (a *^ c) hcf (b *^ c) = d *^ (((a *^ c) hcf (b *^ c)) div^ d) by Th11
.= ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c by ORDINAL3:58 ;
then ( ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c divides a *^ c & ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c divides b *^ c ) by Def5;
then ( (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = a *^ c & (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = b *^ c ) by Th11;
then ( (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c))) *^ c = a *^ c & (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c))) *^ c = b *^ c ) by ORDINAL3:58;
then ( ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = a & ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = b ) by A1, ORDINAL3:36;
then ( (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a & (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides b ) by Def3;
then (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a hcf b by Def5;
then ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d))) = a hcf b by Th11;
then (a hcf b) *^ ((((a *^ c) hcf (b *^ c)) div^ d) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)))) = a hcf b by ORDINAL3:58
.= (a hcf b) *^ 1 by ORDINAL2:56 ;
then ( a hcf b = {} or (((a *^ c) hcf (b *^ c)) div^ d) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d))) = 1 ) by ORDINAL3:36;
then ((a *^ c) hcf (b *^ c)) div^ d = 1 by A1, Th20, ORDINAL3:41;
hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by A2, ORDINAL2:56; :: thesis: verum

end;

suppose a = {} ; :: thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

then ( a hcf b = b & a *^ c = {} ) by Th19, ORDINAL2:52;
hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by Th19; :: thesis: verum

end;

end;