let x, y, z be complex-valued FinSequence; :: thesis: ( len x = len y & len y = len z implies x + (y - z) = (x + y) - z )
assume A1: ( len x = len y & len y = len z ) ; :: thesis: x + (y - z) = (x + y) - z
len (- z) = len z by Th5;
hence x + (y - z) = (x + y) - z by A1, Th24; :: thesis: verum