let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 & a ** A c= a ** B holds
A c= B
let a be Complex; :: thesis: ( a <> 0 & a ** A c= a ** B implies A c= B )
assume that
A1: a <> 0 and
A2: a ** A c= a ** B ; :: 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 a * z in a ** A by Th193;
then ex c being Complex st
( a * z = a * c & c in B ) by A2, Th195;
hence z in B by A1, XCMPLX_1:5; :: thesis: verum