let z be Element of F_Complex ; :: thesis: - z = (- (1_ F_Complex )) * z
reconsider z9 = z as Element of COMPLEX by Def1;
A1: - 1r = - (1_ F_Complex ) by Lm1, Th4;
thus - z = - z9 by Th4
.= (- (1_ F_Complex )) * z by A1 ; :: thesis: verum