let G be addGroup; :: thesis: for a being Element of G holds a * (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
let a be Element of G; :: thesis: a * (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
set A = a * (carr ((Omega). G));
set B = { b where b is Element of G : a,b are_conjugated } ;
thus a * (carr ((Omega). G)) c= { b where b is Element of G : a,b are_conjugated } :: according to XBOOLE_0:def 10 :: thesis: { b where b is Element of G : a,b are_conjugated } c= a * (carr ((Omega). G))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a * (carr ((Omega). G)) or x in { b where b is Element of G : a,b are_conjugated } )
assume A1: x in a * (carr ((Omega). G)) ; :: thesis: x in { b where b is Element of G : a,b are_conjugated }
then reconsider b = x as Element of G ;
ex g being Element of G st
( x = a * g & g in carr ((Omega). G) ) by A1, ThB42;
then b,a are_conjugated ;
hence x in { b where b is Element of G : a,b are_conjugated } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { b where b is Element of G : a,b are_conjugated } or x in a * (carr ((Omega). G)) )
assume x in { b where b is Element of G : a,b are_conjugated } ; :: thesis: x in a * (carr ((Omega). G))
then consider b being Element of G such that
A2: x = b and
A3: a,b are_conjugated ;
ex g being Element of G st b = a * g by A3, Def7;
hence x in a * (carr ((Omega). G)) by A2, ThB42; :: thesis: verum