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
len (- y) = len y by Th5;
then - (x - y) = (- x) + (- (- y)) by A1, Th29
.= (- x) + y ;
hence - (x - y) = (- x) + y ; :: thesis: verum