let p, q be complex-valued FinSequence; |.(p ^ q).| = |.p.| ^ |.q.|
A1:
dom |.(p ^ q).| = Seg (len |.(p ^ q).|)
by FINSEQ_1:def 3;
A2:
now for n being Nat st n in dom |.(p ^ q).| holds
|.(p ^ q).| . n = (|.p.| ^ |.q.|) . nlet n be
Nat;
( n in dom |.(p ^ q).| implies |.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1 )A3:
len |.p.| = len p
by Def2;
assume A4:
n in dom |.(p ^ q).|
;
|.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1then A5:
n >= 1
by A1, FINSEQ_1:1;
A6:
len |.(p ^ q).| = len (p ^ q)
by Def2;
then A7:
n in dom (p ^ q)
by A1, A4, FINSEQ_1:def 3;
per cases
( n in dom p or not n in dom p )
;
suppose
not
n in dom p
;
|.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1then A11:
n > 0 + (len p)
by A5, FINSEQ_3:25;
then A12:
n - (len p) > 0
by XREAL_1:20;
A13:
n =
(len p) + (n - (len p))
.=
(len p) + (n -' (len p))
by A12, XREAL_0:def 2
;
n <= len (p ^ q)
by A1, A4, A6, FINSEQ_1:1;
then
n <= (len q) + (len p)
by FINSEQ_1:22;
then
n - (len p) <= len q
by XREAL_1:20;
then A14:
n -' (len p) <= len q
by XREAL_0:def 2;
1
+ (len p) <= n
by A11, NAT_1:13;
then
1
<= n - (len p)
by XREAL_1:19;
then
1
<= n -' (len p)
by XREAL_0:def 2;
then A15:
n -' (len p) in Seg (len q)
by A14, FINSEQ_1:1;
then A16:
n -' (len p) in dom q
by FINSEQ_1:def 3;
len |.q.| = len q
by Def2;
then A17:
n -' (len p) in dom |.q.|
by A15, FINSEQ_1:def 3;
A18:
(p ^ q) . n = q . (n -' (len p))
by A13, A16, FINSEQ_1:def 7;
thus |.(p ^ q).| . n =
|.((p ^ q) . n).|
by A7, Def2
.=
|.q.| . (n -' (len p))
by A16, A18, Def2
.=
(|.p.| ^ |.q.|) . n
by A3, A13, A17, FINSEQ_1:def 7
;
verum end; end;
len |.(p ^ q).| =
len (p ^ q)
by Def2
.=
(len p) + (len q)
by FINSEQ_1:22
.=
(len p) + (len |.q.|)
by Def2
.=
(len |.p.|) + (len |.q.|)
by Def2
.=
len (|.p.| ^ |.q.|)
by FINSEQ_1:22
;
hence
|.(p ^ q).| = |.p.| ^ |.q.|
by A2, FINSEQ_2:9; verum