let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 & A /// a c= B /// a holds
A c= B
let a be Complex; :: thesis: ( a <> 0 & A /// a c= B /// a implies A c= B )
assume that
A1: a <> 0 and
A2: A /// a c= B /// a ; :: thesis: A c= B
let z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in A or z in B )
assume z in A ; :: thesis: z in B
then z / a in A /// a by Th226;
then ex c being Complex st
( z / a = c / a & c in B ) by A2, Th228;
hence z in B by A1, XCMPLX_1:5; :: thesis: verum