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