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