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