let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for m1, m2 being AlgSequence of L st len m1 = len m2 holds
len (m1 * m2) = len m1
let m1, m2 be AlgSequence of L; :: thesis: ( len m1 = len m2 implies len (m1 * m2) = len m1 )
set p = m1 * m2;
assume A1: len m1 = len m2 ; :: thesis: len (m1 * m2) = len m1

A2: now :: thesis: ( ( len m1 = 0 & len (m1 * m2) >= len m1 ) or ( len m1 <> 0 & len (m1 * m2) >= len m1 ) )

per cases ( len m1 = 0 or len m1 <> 0 ) ;

case len m1 = 0 ; :: thesis: len (m1 * m2) >= len m1

hence len (m1 * m2) >= len m1 ; :: thesis: verum

end;

case len m1 <> 0 ; :: thesis: len (m1 * m2) >= len m1

then len m1 >= 0 + 1 by NAT_1:13;
then (len m1) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider l = (len m1) - 1 as Element of NAT by INT_1:3;
A3: l + 1 = (len m1) + 0 ;
then ( m1 . l <> 0. L & m2 . l <> 0. L ) by A1, ALGSEQ_1:10;
then (m1 . l) * (m2 . l) <> 0. L by VECTSP_2:def 1;
then (m1 * m2) . l <> 0. L by LOPBAN_3:def 7;
hence len (m1 * m2) >= len m1 by A3, Th7; :: thesis: verum

end;

end;

end;

min ((len m1),(len m2)) = len m1 by A1;
then len (m1 * m2) <= len m1 by Th11;
hence len (m1 * m2) = len m1 by A2, XXREAL_0:1; :: thesis: verum