let A, B be complex-membered set ; :: thesis: for a being complex number st a <> 0 & A /// a = B /// a holds
A = B
let a be complex number ; :: thesis: ( a <> 0 & A /// a = B /// a implies A = B )
assume ( a <> 0 & A /// a = B /// a ) ; :: thesis: A = B
then ( A c= B & B c= A ) by Th235;
hence A = B by XBOOLE_0:def 10; :: thesis: verum