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 by Th3;

A2: len (c * x) = len x by Th3;

((- c) * x) + (c * x) = (((- 1) * c) * x) + (c * x)

.= (- (c * x)) + (c * x) by Th44

.= - ((c * x) - (c * x)) by A2, Th32

.= - (0c (len x)) by A2, Th28

.= 0c (len x) by Lm3 ;

hence (- c) * x = - (c * x) by A1, A2, Th26; :: thesis: verum

let c be Complex; :: thesis: (- c) * x = - (c * x)

A1: len ((- c) * x) = len x by Th3;

A2: len (c * x) = len x by Th3;

((- c) * x) + (c * x) = (((- 1) * c) * x) + (c * x)

.= (- (c * x)) + (c * x) by Th44

.= - ((c * x) - (c * x)) by A2, Th32

.= - (0c (len x)) by A2, Th28

.= 0c (len x) by Lm3 ;

hence (- c) * x = - (c * x) by A1, A2, Th26; :: thesis: verum