let p, q be complex-valued FinSequence; :: thesis: |.(p ^ q).| = |.p.| ^ |.q.|
A1: dom |.(p ^ q).| = Seg (len |.(p ^ q).|) by FINSEQ_1:def 3;

A2: now :: thesis: for n being Nat st n in dom |.(p ^ q).| holds
|.(p ^ q).| . n = (|.p.| ^ |.q.|) . n

let n be Nat; :: thesis: ( n in dom |.(p ^ q).| implies |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁ )
A3: len |.p.| = len p by Def2;
assume A4: n in dom |.(p ^ q).| ; :: thesis: |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁
then 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 A8: n in dom p ; :: thesis: |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁

A9: (p ^ q) . n = p . n by A8, FINSEQ_1:def 7;
A10: n in dom |.p.| by A3, A8, FINSEQ_3:29;
thus |.(p ^ q).| . n = |.((p ^ q) . n).| by A7, Def2
.= |.p.| . n by A8, A9, Def2
.= (|.p.| ^ |.q.|) . n by A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose not n in dom p ; :: thesis: |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁

then 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 ; :: thesis: verum

end;

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; :: thesis: verum