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 that
A1: len x = len y and
A2: len y = len z ; :: thesis: x - (y - z) = (x - y) + z
A3: len (- y) = len y by Th5;
x - (y - z) = x + ((- y) + z) by A2, Th39
.= (x - y) + z by A1, A2, A3, Th28 ;
hence x - (y - z) = (x - y) + z ; :: thesis: verum