( z <> 0 implies for x, y being Real st z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i> ) & 0 <= x & x < 2 * PI & z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * <i> ) & 0 <= y & y < 2 * PI holds
x = y )

proof

assume z <> 0 ; :: thesis: for x, y being Real st z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i> ) & 0 <= x & x < 2 * PI & z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * <i> ) & 0 <= y & y < 2 * PI holds
x = y
then A31: |.z.| <> 0 by COMPLEX1:131;
let x, y be Real; :: thesis: ( z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i> ) & 0 <= x & x < 2 * PI & z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * <i> ) & 0 <= y & y < 2 * PI implies x = y )
assume that
A32: z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i> ) and
A33: 0 <= x and
A34: x < 2 * PI and
A35: z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * <i> ) and
A36: 0 <= y and
A37: y < 2 * PI ; :: thesis: x = y
( |.z.| * (cos x) = |.z.| * (cos y) & |.z.| * (sin x) = |.z.| * (sin y) ) by A32, A35, COMPLEX1:163;
then ( cos x = cos y & sin x = sin y ) by A31, XCMPLX_1:5;
then A38: ( cos x = cos y & sin x = sin . y ) by SIN_COS:def 21;
then ( cos x = cos . y & sin . x = sin . y ) by SIN_COS:def 21, SIN_COS:def 23;
then A39: ( cos . x = cos . y & sin . x = sin . y ) by SIN_COS:def 23;

now

per cases ( ( x <= PI & y <= PI ) or ( x > PI & y > PI ) or ( x <= PI & y > PI ) or ( y <= PI & x > PI ) ) ;

suppose ( x <= PI & y <= PI ) ; :: thesis: not x <> y

then ( x in [.0 ,PI .] & y in [.0 ,PI .] ) by A33, A36, XXREAL_1:1;
then A41: ( x in [.0 ,PI .] /\ (dom cos ) & y in [.0 ,PI .] /\ (dom cos ) ) by SIN_COS:27, XBOOLE_0:def 4;
assume x <> y ; :: thesis: contradiction
then ( x < y or y < x ) by XXREAL_0:1;
hence contradiction by A39, A41, Th41, RFUNCT_2:44; :: thesis: verum

end;

suppose ( x > PI & y > PI ) ; :: thesis: not x <> y

then ( x in [.PI ,(2 * PI ).] & y in [.PI ,(2 * PI ).] ) by A34, A37, XXREAL_1:1;
then A42: ( x in [.PI ,(2 * PI ).] /\ (dom cos ) & y in [.PI ,(2 * PI ).] /\ (dom cos ) ) by SIN_COS:27, XBOOLE_0:def 4;
assume x <> y ; :: thesis: contradiction
then ( x < y or y < x ) by XXREAL_0:1;
hence contradiction by A39, A42, Th42, RFUNCT_2:43; :: thesis: verum

end;

suppose ( x <= PI & y > PI ) ; :: thesis: x = y

then ( x in [.0 ,PI .] & y in ].PI ,(2 * PI ).[ ) by A33, A37, XXREAL_1:1, XXREAL_1:4;
then ( sin . x >= 0 & sin . y < 0 ) by Th24, Th25;
hence x = y by A38, SIN_COS:def 21; :: thesis: verum

end;

suppose ( y <= PI & x > PI ) ; :: thesis: x = y

then ( y in [.0 ,PI .] & x in ].PI ,(2 * PI ).[ ) by A34, A36, XXREAL_1:1, XXREAL_1:4;
then ( sin . y >= 0 & sin . x < 0 ) by Th24, Th25;
hence x = y by A38, SIN_COS:def 21; :: thesis: verum

end;

end;

end;

hence x = y ; :: thesis: verum

end;

hence for b₁, b₂ being Real holds
( ( z <> 0 & z = (|.z.| * (cos b₁)) + ((|.z.| * (sin b₁)) * <i> ) & 0 <= b₁ & b₁ < 2 * PI & z = (|.z.| * (cos b₂)) + ((|.z.| * (sin b₂)) * <i> ) & 0 <= b₂ & b₂ < 2 * PI implies b₁ = b₂ ) & ( not z <> 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ; :: thesis: verum