( 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 A27: |.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
A28: z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i> ) and
A29: 0 <= x and
A30: x < 2 * PI and
A31: z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * <i> ) and
A32: 0 <= y and
A33: y < 2 * PI ; :: thesis: x = y
|.z.| * (cos x) = |.z.| * (cos y) by A28, A31, COMPLEX1:163;
then cos x = cos y by A27, XCMPLX_1:5;
then cos x = cos . y by SIN_COS:def 23;
then A34: cos . x = cos . y by SIN_COS:def 23;
|.z.| * (sin x) = |.z.| * (sin y) by A28, A31, COMPLEX1:163;
then sin x = sin y by A27, XCMPLX_1:5;
then A35: sin x = sin . y by SIN_COS:def 21;

now

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

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

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

end;

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

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

end;

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

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

end;

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

then x in ].PI ,(2 * PI ).[ by A30, XXREAL_1:4;
then A45: sin . x < 0 by Th25;
y in [.0 ,PI .] by A32, A44, XXREAL_1:1;
then sin . y >= 0 by Th24;
hence x = y by A35, A45, 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