let a, b be Integer; :: thesis: Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b)))

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

suppose ( a = 0 & b = 0 ) ; :: thesis: Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b)))

then ( Parity (a gcd b) = 0 & Parity (a + b) = 0 ) by Def1;
hence Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b))) ; :: thesis: verum

end;

suppose A1: ( a <> 0 or b <> 0 ) ; :: thesis: Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b)))

Parity (((a + b) / (a gcd b)) * (a gcd b)) = (Parity ((a + b) / (a gcd b))) * (Parity (a gcd b)) by ILP;
hence Parity (a + b) = (Parity (a gcd b)) * (Parity ((a + b) / (a gcd b))) by A1, XCMPLX_1:87; :: thesis: verum

end;

end;