let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st c <> 0. R & c divides a & c divides b & c divides a + b holds
(a / c) + (b / c) = (a + b) / c
let a, b, c be Element of R; :: thesis: ( c <> 0. R & c divides a & c divides b & c divides a + b implies (a / c) + (b / c) = (a + b) / c )
assume A1: c <> 0. R ; :: thesis: ( not c divides a or not c divides b or not c divides a + b or (a / c) + (b / c) = (a + b) / c )
assume A2: ( c divides a & c divides b & c divides a + b ) ; :: thesis: (a / c) + (b / c) = (a + b) / c
set d = a / c;
set e = b / c;
A3: (a / c) * c = a by A1, A2, Def4;
(b / c) * c = b by A1, A2, Def4;
then a + b = ((a / c) + (b / c)) * c by A3, VECTSP_1:def 12;
then (a + b) / c = ((a / c) + (b / c)) * (c / c) by A1, A2, Th11
.= ((a / c) + (b / c)) * (1. R) by A1, Th9
.= (a / c) + (b / c) by VECTSP_1:def 13 ;
hence (a / c) + (b / c) = (a + b) / c ; :: thesis: verum