let x be FinSequence of COMPLEX ; :: thesis: for c being Complex holds - (c * x) = c * (- x)
let c be Complex; :: thesis: - (c * x) = c * (- x)
A1: ( len (c * (- x)) = len (- x) & len (c * x) = len x ) by Th3;
A2: len x = len (- x) by Th5;
then (c * (- x)) + (c * x) = c * (x + (- x)) by Th25
.= c * (0c (len x)) by Th28
.= 0c (len x) by Th34 ;
hence - (c * x) = c * (- x) by A2, A1, Th26; :: thesis: verum