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 set ; :: 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 & a in A * B & b in C ) ;
consider g, h being Element of G such that
A2: ( a = g * h & g in A & h in B ) by A1;
( x = (g |^ b) * (h |^ b) & g |^ b in A |^ C & h |^ b in B |^ C ) by A1, A2, Th28;
hence x in (A |^ C) * (B |^ C) ; :: thesis: verum