let m1, m2 be complex-valued FinSequence; :: thesis: ( len m1 = len m2 implies for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k) )

assume A1: len m1 = len m2 ; :: thesis: for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)

let k9 be Nat; :: thesis: ( k9 <= len m1 implies (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9) )
set p = (m1 (#) m2) | k9;
set q = (m1 | k9) (#) (m2 | k9);
assume A2: k9 <= len m1 ; :: thesis: (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9)
then A3: len (m1 | k9) = k9 by FINSEQ_1:59;
reconsider k = k9 as Element of NAT by ORDINAL1:def 12;
A4: k9 <= len (m1 (#) m2) by A1, A2, Lm4;
then A5: len ((m1 (#) m2) | k9) = k9 by FINSEQ_1:59;
A6: len (m2 | k9) = k9 by ;
then A7: len ((m1 | k9) (#) (m2 | k9)) = k9 by ;
now :: thesis: for j being Nat st 1 <= j & j <= len ((m1 (#) m2) | k9) holds
((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . j
A8: len (m1 (#) m2) = len m1 by ;
let j be Nat; :: thesis: ( 1 <= j & j <= len ((m1 (#) m2) | k9) implies ((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . j )
assume that
A9: 1 <= j and
A10: j <= len ((m1 (#) m2) | k9) ; :: thesis: ((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . j
A11: j in Seg k by A5, A9, A10;
then A12: j in dom (m1 | k) by ;
A13: j in dom ((m1 | k9) (#) (m2 | k9)) by ;
A14: j in dom (m2 | k) by ;
j <= len m1 by ;
then j in Seg (len (m1 (#) m2)) by A9, A8;
then A15: j in dom (m1 (#) m2) by FINSEQ_1:def 3;
j in dom ((m1 (#) m2) | k9) by ;
hence ((m1 (#) m2) | k9) . j = (m1 (#) m2) . j by FUNCT_1:47
.= (m1 . j) * (m2 . j) by
.= ((m1 | k) . j) * (m2 . j) by
.= ((m1 | k) . j) * ((m2 | k) . j) by
.= ((m1 | k9) (#) (m2 | k9)) . j by ;
:: thesis: verum
end;
hence (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9) by ; :: thesis: verum