let G be commutative Group; :: thesis: for A, B being Subset of G holds (A * B) " = (A ") * (B ")

let A, B be Subset of G; :: thesis: (A * B) " = (A ") * (B ")

thus (A * B) " c= (A ") * (B ") :: according to XBOOLE_0:def 10 :: thesis: (A ") * (B ") c= (A * B) "

assume x in (A ") * (B ") ; :: thesis: x in (A * B) "

then consider g1, g2 being Element of G such that

A6: x = g1 * g2 and

A7: g1 in A " and

A8: g2 in B " ;

consider b being Element of G such that

A9: g2 = b " and

A10: b in B by A8;

consider a being Element of G such that

A11: g1 = a " and

A12: a in A by A7;

A13: a * b in A * B by A12, A10;

x = (a * b) " by A6, A11, A9, GROUP_1:47;

hence x in (A * B) " by A13; :: thesis: verum

let A, B be Subset of G; :: thesis: (A * B) " = (A ") * (B ")

thus (A * B) " c= (A ") * (B ") :: according to XBOOLE_0:def 10 :: thesis: (A ") * (B ") c= (A * B) "

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ") * (B ") or x in (A * B) " )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A * B) " or x in (A ") * (B ") )

assume x in (A * B) " ; :: thesis: x in (A ") * (B ")

then consider g being Element of G such that

A1: x = g " and

A2: g in A * B ;

consider g1, g2 being Element of G such that

A3: g = g1 * g2 and

A4: ( g1 in A & g2 in B ) by A2;

A5: ( g1 " in A " & g2 " in B " ) by A4;

x = (g1 ") * (g2 ") by A1, A3, GROUP_1:47;

hence x in (A ") * (B ") by A5; :: thesis: verum

end;assume x in (A * B) " ; :: thesis: x in (A ") * (B ")

then consider g being Element of G such that

A1: x = g " and

A2: g in A * B ;

consider g1, g2 being Element of G such that

A3: g = g1 * g2 and

A4: ( g1 in A & g2 in B ) by A2;

A5: ( g1 " in A " & g2 " in B " ) by A4;

x = (g1 ") * (g2 ") by A1, A3, GROUP_1:47;

hence x in (A ") * (B ") by A5; :: thesis: verum

assume x in (A ") * (B ") ; :: thesis: x in (A * B) "

then consider g1, g2 being Element of G such that

A6: x = g1 * g2 and

A7: g1 in A " and

A8: g2 in B " ;

consider b being Element of G such that

A9: g2 = b " and

A10: b in B by A8;

consider a being Element of G such that

A11: g1 = a " and

A12: a in A by A7;

A13: a * b in A * B by A12, A10;

x = (a * b) " by A6, A11, A9, GROUP_1:47;

hence x in (A * B) " by A13; :: thesis: verum