let X be set ; :: thesis: for A, B being complex-membered set st X = { (c1 * c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } holds
X = { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) }
let A, B be complex-membered set ; :: thesis: ( X = { (c1 * c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } implies X = { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } )
assume A1: X = { (c1 * c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } ; :: thesis: X = { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) }
thus X c= { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } :: according to XBOOLE_0:def 10 :: thesis: { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } c= X
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in X or e in { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } )
assume e in X ; :: thesis: e in { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) }
then ex c1, c2 being Complex st
( e = c1 * c2 & c1 in A & c2 in B ) by A1;
hence e in { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } ; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } or e in X )
assume e in { (c1 * c2) where c1, c2 is Complex : ( c1 in B & c2 in A ) } ; :: thesis: e in X
then ex c1, c2 being Complex st
( e = c1 * c2 & c1 in B & c2 in A ) ;
hence e in X by A1; :: thesis: verum