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, Th2;
thus - z = - z9 by Th2
.= (- (1_ F_Complex)) * z by A1 ; :: thesis: verum