let A, B be complex-membered set ; for a being Complex st a <> 0 & a /// A c= a /// B holds
A c= B
let a be Complex; ( a <> 0 & a /// A c= a /// B implies A c= B )
assume that
A1:
a <> 0
and
A2:
a /// A c= a /// B
; A c= B
let z be Complex; MEMBERED:def 7 ( not z in A or z in B )
assume
z in A
; z in B
then
a / z in a /// A
by Th213;
then consider c being Complex such that
A3:
a / z = a / c
and
A4:
c in B
by A2, Th215;
z " = c "
by A1, A3, XCMPLX_1:5;
hence
z in B
by A4, XCMPLX_1:201; verum