let R be commutative domRing-like Ring; :: thesis: for a, b, c, d being Element of R st b <> 0. R & d <> 0. R & b divides a & d divides c holds
(a / b) * (c / d) = (a * c) / (b * d)
let a, b, c, d be Element of R; :: thesis: ( b <> 0. R & d <> 0. R & b divides a & d divides c implies (a / b) * (c / d) = (a * c) / (b * d) )
assume A1: ( b <> 0. R & d <> 0. R & b divides a & d divides c ) ; :: thesis: (a / b) * (c / d) = (a * c) / (b * d)
set x = a / b;
set y = c / d;
set z = (a * c) / (b * d);
A2: (a / b) * b = a by A1, Def4;
A3: (c / d) * d = c by A1, Def4;
A4: b * d divides a * c by A1, Th3;
A5: b * d <> 0. R by A1, VECTSP_2:def 5;
then ((a * c) / (b * d)) * (b * d) = ((a / b) * b) * ((c / d) * d) by A2, A3, A4, Def4
.= (a / b) * (b * ((c / d) * d)) by GROUP_1:def 4
.= (a / b) * ((c / d) * (b * d)) by GROUP_1:def 4
.= ((a / b) * (c / d)) * (b * d) by GROUP_1:def 4 ;
hence (a / b) * (c / d) = (a * c) / (b * d) by A5, Th1; :: thesis: verum