let x, y be complex-valued FinSequence; :: thesis: ( len x = len y implies - (x + y) = (- x) + (- y) )
assume A1: len x = len y ; :: thesis: - (x + y) = (- x) + (- y)
A2: len (- y) = len y by Th5;
then A3: len ((- x) + (- y)) = len (- x) by A1, Th5, Th6;
A4: len (- x) = len x by Th5;
A5: len (x + y) = len x by A1, Th6;
then (x + y) + ((- x) + (- y)) = ((y + x) + (- x)) + (- y) by A1, A2, A4, Th24
.= (y + (x + (- x))) + (- y) by A1, A4, Th24
.= (y + (0c (len x))) + (- y) by Th28
.= y + (- y) by A1, Th27
.= 0c (len y) by Th28 ;
hence - (x + y) = (- x) + (- y) by A1, A4, A5, A3, Th26; :: thesis: verum