( 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:45;
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:77;
then cos x = cos y by A27, XCMPLX_1:5;
then cos x = cos . y by SIN_COS:def 19;
then A34: cos . x = cos . y by SIN_COS:def 19;
|.z.| * (sin x) = |.z.| * (sin y) by A28, A31, COMPLEX1:77;
then sin x = sin y by A27, XCMPLX_1:5;
then A35: sin x = sin . y by SIN_COS:def 17;

now :: thesis: not x <> y

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:24, 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:24, XBOOLE_0:def 4;
hence contradiction by A34, A37, A38, Th25, RFUNCT_2:21; :: 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:24, 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:24, XBOOLE_0:def 4;
hence contradiction by A34, A40, A41, Th26, RFUNCT_2:20; :: 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 Th9;
x in [.0,PI.] by A29, A42, XXREAL_1:1;
then sin . x >= 0 by Th8;
hence x = y by A35, A43, SIN_COS:def 17; :: 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 Th9;
y in [.0,PI.] by A32, A44, XXREAL_1:1;
then sin . y >= 0 by Th8;
hence x = y by A35, A45, SIN_COS:def 17; :: 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