let m1, m2 be complex-valued FinSequence; :: thesis: ( len m1 = len m2 implies for k being natural number st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k) )
assume A1: len m1 = len m2 ; :: thesis: for k being natural number st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
let k' be natural number ; :: thesis: ( k' <= len m1 implies (m1 (#) m2) | k' = (m1 | k') (#) (m2 | k') )
set p = (m1 (#) m2) | k';
set q = (m1 | k') (#) (m2 | k');
assume A2: k' <= len m1 ; :: thesis: (m1 (#) m2) | k' = (m1 | k') (#) (m2 | k')
then A3: len (m1 | k') = k' by FINSEQ_1:80;
reconsider k = k' as Element of NAT by ORDINAL1:def 13;
A4: k' <= len (m1 (#) m2) by A1, A2, Lm4;
then A5: len ((m1 (#) m2) | k') = k' by FINSEQ_1:80;
A6: len (m2 | k') = k' by A1, A2, FINSEQ_1:80;
then A7: len ((m1 | k') (#) (m2 | k')) = k' by A3, Lm4;

now

A8: len (m1 (#) m2) = len m1 by A1, Lm4;
let j be Nat; :: thesis: ( 1 <= j & j <= len ((m1 (#) m2) | k') implies ((m1 (#) m2) | k') . j = ((m1 | k') (#) (m2 | k')) . j )
assume that
A9: 1 <= j and
A10: j <= len ((m1 (#) m2) | k') ; :: thesis: ((m1 (#) m2) | k') . j = ((m1 | k') (#) (m2 | k')) . j
A11: j in NAT by ORDINAL1:def 13;
then A12: j in Seg k by A5, A9, A10;
then A13: j in dom (m1 | k) by A3, FINSEQ_1:def 3;
A14: j in dom ((m1 | k') (#) (m2 | k')) by A7, A12, FINSEQ_1:def 3;
A15: j in dom (m2 | k) by A6, A12, FINSEQ_1:def 3;
j <= len m1 by A2, A5, A10, XXREAL_0:2;
then j in Seg (len (m1 (#) m2)) by A9, A11, A8;
then A16: j in dom (m1 (#) m2) by FINSEQ_1:def 3;
j in dom ((m1 (#) m2) | k') by A9, A10, FINSEQ_3:27;
hence ((m1 (#) m2) | k') . j = (m1 (#) m2) . j by FUNCT_1:70
.= (m1 . j) * (m2 . j) by A16, VALUED_1:def 4
.= ((m1 | k) . j) * (m2 . j) by A13, FUNCT_1:70
.= ((m1 | k) . j) * ((m2 | k) . j) by A15, FUNCT_1:70
.= ((m1 | k') (#) (m2 | k')) . j by A14, VALUED_1:def 4 ;
:: thesis: verum

end;

hence (m1 (#) m2) | k' = (m1 | k') (#) (m2 | k') by A4, A7, FINSEQ_1:18, FINSEQ_1:80; :: thesis: verum