let m1, m2 be complex-valued FinSequence; :: thesis: ( len m1 = len m2 implies len (m1 + m2) = len m1 )
assume A1: len m1 = len m2 ; :: thesis: len (m1 + m2) = len m1
thus len (m1 + m2) = min ((len m1),(len m2)) by Th1
.= len m1 by A1 ; :: thesis: verum