let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st c <> 0. R holds
( ( c divides a * b & c divides a implies (a * b) / c = (a / c) * b ) & ( c divides a * b & c divides b implies (a * b) / c = a * (b / c) ) )
let A, B, C be Element of R; :: thesis: ( C <> 0. R implies ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) ) )
assume A1: C <> 0. R ; :: thesis: ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) )

A2: now

assume A3: ( C divides A * B & C divides A ) ; :: thesis: ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B )
set A1 = (A * B) / C;
A4: ((A * B) / C) * C = A * B by A1, A3, Def4;
set A2 = A / C;
(A / C) * C = A by A1, A3, Def4;
then ((A * B) / C) * C = ((A / C) * B) * C by A4, GROUP_1:def 4;
hence ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) by A1, Th1; :: thesis: verum

end;

now

assume A5: ( C divides A * B & C divides B ) ; :: thesis: ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) )
set A1 = (A * B) / C;
A6: ((A * B) / C) * C = A * B by A1, A5, Def4;
set A2 = B / C;
(B / C) * C = B by A1, A5, Def4;
then ((A * B) / C) * C = (A * (B / C)) * C by A6, GROUP_1:def 4;
hence ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) by A1, Th1; :: thesis: verum

end;

hence ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) ) by A2; :: thesis: verum