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 (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 Th30
.= c * (0c (len x)) by Th34
.= 0c (len x) by Th41 ;
hence - (c * x) = c * (- x) by A2, A1, Th32; :: thesis: verum