let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min (len m1),(len m2)
let m1, m2 be AlgSequence of L; :: thesis: len (m1 * m2) <= min (len m1),(len m2)
set p = m1 * m2;
set k = min (len m1),(len m2);
reconsider k = min (len m1),(len m2) as Element of NAT by XXREAL_0:15;

now

let i be Nat; :: thesis: ( i >= k implies 0. L = (m1 * m2) . b₁ )
assume A1: i >= k ; :: thesis: 0. L = (m1 * m2) . b₁

per cases ( k = len m1 or k = len m2 ) by XXREAL_0:15;

suppose k = len m1 ; :: thesis: 0. L = (m1 * m2) . b₁

then m1 . i = 0. L by A1, ALGSEQ_1:22;
hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:39
.= (m1 * m2) . i by Def2 ;
:: thesis: verum

end;

suppose k = len m2 ; :: thesis: 0. L = (m1 * m2) . b₁

then m2 . i = 0. L by A1, ALGSEQ_1:22;
hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:36
.= (m1 * m2) . i by Def2 ;
:: thesis: verum

end;

end;

end;

then k is_at_least_length_of m1 * m2 by ALGSEQ_1:def 3;
hence len (m1 * m2) <= min (len m1),(len m2) by ALGSEQ_1:def 4; :: thesis: verum