let x be FinSequence of COMPLEX ; :: thesis: for c being complex number holds - (c * x) = c * (- x)
let c be complex number ; :: thesis: - (c * x) = c * (- x)
A1: len x = len (- x) by Th5;
A2: len (c * (- x)) = len (- x) by Th3;
A3: len (c * x) = len x by Th3;
(c * (- x)) + (c * x) = c * (x + (- x)) by A1, Th30
.= c * (0c (len x)) by Th34
.= 0c (len x) by Th41 ;
hence - (c * x) = c * (- x) by A1, A2, A3, Th32; :: thesis: verum