let a, b be non zero Integer; :: thesis: a gcd b = ((Parity a) gcd (Parity b)) * ((Oddity a) gcd (Oddity b))
a gcd b = ((Parity a) * (Oddity a)) gcd b
.= ((Parity a) gcd ((Parity b) * (Oddity b))) * ((Oddity a) gcd b) by NEWTON03:35, OPC
.= (((Parity a) gcd (Parity b)) * ((Parity a) gcd (Oddity b))) * ((Oddity a) gcd b) by NEWTON03:35, OPC
.= (((Parity a) gcd (Parity b)) * 1) * ((Oddity a) gcd b) by OPC
.= ((Parity a) gcd (Parity b)) * ((Oddity a) gcd ((Parity b) * (Oddity b)))
.= ((Parity a) gcd (Parity b)) * (((Oddity a) gcd (Parity b)) * ((Oddity a) gcd (Oddity b))) by NEWTON03:35, OPC
.= ((Parity a) gcd (Parity b)) * (1 * ((Oddity a) gcd (Oddity b))) by OPC ;
hence a gcd b = ((Parity a) gcd (Parity b)) * ((Oddity a) gcd (Oddity b)) ; :: thesis: verum