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 A1: c = {} ; :: thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c

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

end;

suppose A3: ( 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 12;
set e = ((a *^ c) hcf (b *^ c)) div^ d;
a hcf b divides b by Def5;
then b = (a hcf b) *^ (b div^ (a hcf b)) by Th11;
then b *^ c = d *^ (b div^ (a hcf b)) by ORDINAL3:50;
then A4: d divides b *^ c by Def3;
a hcf b divides a by Def5;
then a = (a hcf b) *^ (a div^ (a hcf b)) by Th11;
then a *^ c = d *^ (a div^ (a hcf b)) by ORDINAL3:50;
then d divides a *^ c by Def3;
then d divides (a *^ c) hcf (b *^ c) by A4, Def5;
then A5: (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:50 ;
then ((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) *^ ((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)) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c))) *^ c = b *^ c by ORDINAL3:50;
then ((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 A3, ORDINAL3:33;
then A6: (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides b by Def3;
((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c divides a *^ c by A5, 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 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 by ORDINAL3:50;
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 by A3, ORDINAL3:33;
then (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a by Def3;
then (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a hcf b by A6, 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:50
.= (a hcf b) *^ 1 by ORDINAL2:39 ;
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:33;
then ((a *^ c) hcf (b *^ c)) div^ d = 1 by A3, Th20, ORDINAL3:37;
hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by A5, ORDINAL2:39; :: 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:35;
hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by Th19; :: thesis: verum

end;

end;