let a be Real; :: thesis: ( |.a.| = |.(1 - a).| implies a = 1 / 2 )
assume A1: |.a.| = |.(1 - a).| ; :: thesis: a = 1 / 2
( |.a.| ^2 = a ^2 & |.(1 - a).| ^2 = (1 - a) ^2 ) by COMPLEX1:75;
then a ^2 = (1 - a) * (1 - a) by A1, SQUARE_1:def 1
.= (1 - (2 * a)) + (a * a)
.= (1 - (2 * a)) + (a ^2) by SQUARE_1:def 1 ;
hence a = 1 / 2 ; :: thesis: verum