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 )
set e = b / c;
set d = a / c;
assume that
A2: ( c divides a & c divides b ) and
A3: c divides a + b ; :: thesis: (a / c) + (b / c) = (a + b) / c
( (a / c) * c = a & (b / c) * c = b ) by A1, A2, Def4;
then a + b = ((a / c) + (b / c)) * c by VECTSP_1:def 3;
then (a + b) / c = ((a / c) + (b / c)) * (c / c) by A1, A3, Th11
.= ((a / c) + (b / c)) * (1. R) by A1, Th9
.= (a / c) + (b / c) ;
hence (a / c) + (b / c) = (a + b) / c ; :: thesis: verum