let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 & a ** A = a ** B holds
A = B
let a be Complex; :: thesis: ( a <> 0 & a ** A = a ** B implies A = B )
assume ( a <> 0 & a ** A = a ** B ) ; :: thesis: A = B
then ( A c= B & B c= A ) by Th196;
hence A = B ; :: thesis: verum