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

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