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 by Th3;
A2: len (c * x) = len x by Th3;
((- c) * x) + (c * x) = (((- 1) * c) * x) + (c * x)
.= (- (c * x)) + (c * x) by Th53
.= - ((c * x) - (c * x)) by A2, Th39
.= - (0c (len x)) by A2, Th34
.= 0c (len x) by Lm2 ;
hence (- c) * x = - (c * x) by A1, A2, Th32; :: thesis: verum