let G be Group; :: 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