let R be commutative domRing-like Ring; 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; ( b <> 0. R & d <> 0. R & b divides a & d divides c implies (a / b) * (c / d) = (a * c) / (b * d) )
assume that
A1:
( b <> 0. R & d <> 0. R )
and
A2:
( b divides a & d divides c )
; (a / b) * (c / d) = (a * c) / (b * d)
A3:
b * d divides a * c
by A2, Th3;
set z = (a * c) / (b * d);
set y = c / d;
set x = a / b;
A4:
b * d <> 0. R
by A1, VECTSP_2:def 1;
( (a / b) * b = a & (c / d) * d = c )
by A1, A2, Def4;
then ((a * c) / (b * d)) * (b * d) =
((a / b) * b) * ((c / d) * d)
by A3, A4, Def4
.=
(a / b) * (b * ((c / d) * d))
by GROUP_1:def 3
.=
(a / b) * ((c / d) * (b * d))
by GROUP_1:def 3
.=
((a / b) * (c / d)) * (b * d)
by GROUP_1:def 3
;
hence
(a / b) * (c / d) = (a * c) / (b * d)
by A4, Th1; verum