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 AS1: 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') )
assume AS2: k' <= len m1 ; :: thesis: (m1 (#) m2) | k' = (m1 | k') (#) (m2 | k')
set p = (m1 (#) m2) | k';
set q = (m1 | k') (#) (m2 | k');
H: ( len (m1 | k') = k' & len (m2 | k') = k' ) by AS1, AS2, FINSEQ_1:80;
k' <= len (m1 (#) m2) by AS1, AS2, length3;
then A: ( len ((m1 (#) m2) | k') = k' & len ((m1 | k') (#) (m2 | k')) = k' ) by H, length3, FINSEQ_1:80;
reconsider k = k' as Element of NAT by ORDINAL1:def 13;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len ((m1 (#) m2) | k') implies ((m1 (#) m2) | k') . j = ((m1 | k') (#) (m2 | k')) . j )
assume B1: ( 1 <= j & j <= len ((m1 (#) m2) | k') ) ; :: thesis: ((m1 (#) m2) | k') . j = ((m1 | k') (#) (m2 | k')) . j
then B2: j in dom ((m1 (#) m2) | k') by FINSEQ_3:27;
AA: j in NAT by ORDINAL1:def 13;
then D: j in Seg k by B1, A;
E: j <= len m1 by B1, A, AS2, XXREAL_0:2;
len (m1 (#) m2) = len m1 by AS1, length3;
then j in Seg (len (m1 (#) m2)) by AA, E, B1;
then B3: j in dom (m1 (#) m2) by FINSEQ_1:def 3;
B6: j in dom (m1 | k) by D, H, FINSEQ_1:def 3;
B7: j in dom (m2 | k) by D, H, FINSEQ_1:def 3;
B8: j in dom ((m1 | k') (#) (m2 | k')) by D, A, FINSEQ_1:def 3;
thus ((m1 (#) m2) | k') . j = (m1 (#) m2) . j by B2, FUNCT_1:70
.= (m1 . j) * (m2 . j) by B3, VALUED_1:def 4
.= ((m1 | k) . j) * (m2 . j) by B6, FUNCT_1:70
.= ((m1 | k) . j) * ((m2 | k) . j) by B7, FUNCT_1:70
.= ((m1 | k') (#) (m2 | k')) . j by B8, VALUED_1:def 4 ; :: thesis: verum

end;

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