let a, b be natural Ordinal; :: thesis: ( ( a <> {} or b <> {} ) implies a div^ (a hcf b),b div^ (a hcf b) are_relative_prime )
assume A1: ( a <> {} or b <> {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime
A2: ( 1 *^ a = a & 1 *^ b = b ) by ORDINAL2:56;
set ab = a hcf b;

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

suppose ( a = {} or b = {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime

then ( ( a hcf b = b & b div^ b = 1 ) or ( a hcf b = a & a div^ a = 1 ) ) by A1, A2, Th19, ORDINAL3:81;
hence a div^ (a hcf b),b div^ (a hcf b) are_relative_prime by Th6; :: thesis: verum

end;

suppose A3: ( a <> {} & b <> {} ) ; :: thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime

( a hcf b divides a & a hcf b divides b ) by Def5;
then A4: ( a = (a hcf b) *^ (a div^ (a hcf b)) & b = (a hcf b) *^ (b div^ (a hcf b)) ) by Th11;
let c, d1, d2 be Ordinal; :: according to ARYTM_3:def 2 :: thesis: ( a div^ (a hcf b) = c *^ d1 & b div^ (a hcf b) = c *^ d2 implies c = 1 )
assume A5: ( a div^ (a hcf b) = c *^ d1 & b div^ (a hcf b) = c *^ d2 ) ; :: thesis: c = 1
( a div^ (a hcf b) <> {} & b div^ (a hcf b) <> {} ) by A3, A4, ORDINAL2:52;
then reconsider c = c, d1 = d1, d2 = d2 as Element of omega by A5, ORDINAL3:88;
( a = ((a hcf b) *^ c) *^ d1 & b = ((a hcf b) *^ c) *^ d2 ) by A4, A5, ORDINAL3:58;
then ( (a hcf b) *^ c divides a & (a hcf b) *^ c divides b ) by Def3;
then (a hcf b) *^ c divides a hcf b by Def5;
then a hcf b = ((a hcf b) *^ c) *^ ((a hcf b) div^ ((a hcf b) *^ c)) by Th11;
then a hcf b = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) by ORDINAL3:58;
then ( (a hcf b) *^ 1 = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) & a hcf b <> {} ) by A3, A4, ORDINAL2:52, ORDINAL2:56;
then 1 = c *^ ((a hcf b) div^ ((a hcf b) *^ c)) by ORDINAL3:36;
hence c = 1 by ORDINAL3:41; :: thesis: verum

end;

end;