let G be addGroup; :: thesis: for A, B, C being Subset of G holds (A + B) * C c= (A * C) + (B * C)
let A, B, C be Subset of G; :: thesis: (A + B) * C c= (A * C) + (B * C)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A + B) * C or x in (A * C) + (B * C) )
assume x in (A + B) * C ; :: thesis: x in (A * C) + (B * C)
then consider a, b being Element of G such that
A1: x = a * b and
A2: a in A + B and
A3: b in C ;
consider g, h being Element of G such that
A4: ( a = g + h & g in A ) and
A5: h in B by A2;
A6: h * b in B * C by A3, A5;
( x = (g * b) + (h * b) & g * b in A * C ) by A1, A3, A4, Th23;
hence x in (A * C) + (B * C) by A6; :: thesis: verum