theorem Th14: :: EC_PF_2:14

for K being Ring
for a1, a2, a3, a4 being Element of K holds
( a1 * ((a2 + a3) + a4) = ((a1 * a2) + (a1 * a3)) + (a1 * a4) & a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) & a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )