let m1, m2 be complex-valued FinSequence; ( 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
; for k being Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
let k9 be Nat; ( 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
; (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 for j being Nat st 1 <= j & j <= len ((m1 (#) m2) | k9) holds
((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . jA8:
len (m1 (#) m2) = len m1
by A1, Lm4;
let j be
Nat;
( 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)
;
((m1 (#) m2) | k9) . j = ((m1 | k9) (#) (m2 | k9)) . jA11:
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
;
verum end;
hence
(m1 (#) m2) | k9 = (m1 | k9) (#) (m2 | k9)
by A4, A7, FINSEQ_1:59; verum