let a be Real; :: thesis: ( 0 <= a & a < 2 * PI & cos a = 1 implies a = 0 )
assume that
A1: ( 0 <= a & a < 2 * PI ) and
A2: cos a = 1 ; :: thesis: a = 0
(1 * 1) + ((sin a) * (sin a)) = 1 by A2, SIN_COS:29;
then sin a = 0 ;
hence a = 0 by A1, A2, Th17, SIN_COS:77; :: thesis: verum