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 Th3
.= len m1 by A1 ; :: thesis: verum