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 ;

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

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 ;

now :: thesis: for i being Nat st i >= k holds

0. L = (m1 * m2) . i

then
k is_at_least_length_of m1 * m2
by ALGSEQ_1:def 2;0. L = (m1 * m2) . i

let i be Nat; :: thesis: ( i >= k implies 0. L = (m1 * m2) . b_{1} )

assume A1: i >= k ; :: thesis: 0. L = (m1 * m2) . b_{1}

end;assume A1: i >= k ; :: thesis: 0. L = (m1 * m2) . b

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