let x, y be FinSequence of COMPLEX ; :: 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, Th35
.= (- x) + y ;
hence - (x - y) = (- x) + y ; :: thesis: verum