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 A1, A2, FINSEQ_1:59;
then A7: len ((m1 | k9) (#) (m2 | k9)) = k9 by A3, Lm4;

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 A1, Lm4;
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 A3, FINSEQ_1:def 3;
A13: j in dom ((m1 | k9) (#) (m2 | k9)) by A7, A11, FINSEQ_1:def 3;
A14: j in dom (m2 | k) by A6, A11, FINSEQ_1:def 3;
j <= len m1 by A2, A5, A10, XXREAL_0:2;
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 A9, A10, FINSEQ_3:25;
hence ((m1 (#) m2) | k9) . j = (m1 (#) m2) . j by FUNCT_1:47
.= (m1 . j) * (m2 . j) by A15, VALUED_1:def 4
.= ((m1 | k) . j) * (m2 . j) by A12, FUNCT_1:47
.= ((m1 | k) . j) * ((m2 | k) . j) by A14, FUNCT_1:47
.= ((m1 | k9) (#) (m2 | k9)) . j by A13, VALUED_1:def 4 ;
:: thesis: verum

end;

hence (m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9) by A4, A7, FINSEQ_1:59; :: thesis: verum