let a, b, c be Nat; :: thesis: ( (a / b) * c is natural & b <> 0 & a,b are_coprime implies ex d being Nat st c = b * d )
assume (a / b) * c is natural ; :: thesis: ( not b <> 0 or not a,b are_coprime or ex d being Nat st c = b * d )
then reconsider n = (a / b) * c as Nat ;
assume that
A1: b <> 0 and
A2: a,b are_coprime ; :: thesis: ex d being Nat st c = b * d
n * b = ((a / b) * b) * c
.= a * c by A1, XCMPLX_1:87 ;
then b divides a * c ;
then b divides c by A2, EULER_1:13;
hence ex d being Nat st c = b * d ; :: thesis: verum