let p, q be FinSequence of the carrier of F_Complex ; :: thesis: |.(p ^ q).| = |.p.| ^ |.q.|
A1: dom |.(p ^ q).| = Seg (len |.(p ^ q).|) by FINSEQ_1:def 3;

A2: now

let n be Nat; :: thesis: ( n in dom |.(p ^ q).| implies |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁ )
A3: len |.p.| = len p by Def1;
assume A4: n in dom |.(p ^ q).| ; :: thesis: |.(p ^ q).| . b₁ = (|.p.| ^ |.q.|) . b₁
then A5: n >= 1 by A1, FINSEQ_1:3;
A6: len |.(p ^ q).| = len (p ^ q) by Def1;
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 ^ q) . n by A7, PARTFUN1:def 8
.= p . n by A8, FINSEQ_1:def 7
.= p /. n by A8, PARTFUN1:def 8 ;
A10: n in dom |.p.| by A3, A8, FINSEQ_3:31;
thus |.(p ^ q).| . n = |.(p ^ q).| /. n by A4, PARTFUN1:def 8
.= |.((p ^ q) /. n).| by A7, Def1
.= |.p.| /. n by A8, A9, Def1
.= |.p.| . n by A10, PARTFUN1:def 8
.= (|.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:27;
then A12: n - (len p) > 0 by XREAL_1:22;
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:3;
then n <= (len q) + (len p) by FINSEQ_1:35;
then n - (len p) <= len q by XREAL_1:22;
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:21;
then 1 <= n -' (len p) by XREAL_0:def 2;
then A15: n -' (len p) in Seg (len q) by A14, FINSEQ_1:3;
then A16: n -' (len p) in dom q by FINSEQ_1:def 3;
len |.q.| = len q by Def1;
then A17: n -' (len p) in dom |.q.| by A15, FINSEQ_1:def 3;
A18: (p ^ q) /. n = (p ^ q) . n by A7, PARTFUN1:def 8
.= q . (n -' (len p)) by A13, A16, FINSEQ_1:def 7
.= q /. (n -' (len p)) by A16, PARTFUN1:def 8 ;
thus |.(p ^ q).| . n = |.(p ^ q).| /. n by A4, PARTFUN1:def 8
.= |.((p ^ q) /. n).| by A7, Def1
.= |.q.| /. (n -' (len p)) by A16, A18, Def1
.= |.q.| . (n -' (len p)) by A17, PARTFUN1:def 8
.= (|.p.| ^ |.q.|) . n by A3, A13, A17, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

len |.(p ^ q).| = len (p ^ q) by Def1
.= (len p) + (len q) by FINSEQ_1:35
.= (len p) + (len |.q.|) by Def1
.= (len |.p.|) + (len |.q.|) by Def1
.= len (|.p.| ^ |.q.|) by FINSEQ_1:35 ;
hence |.(p ^ q).| = |.p.| ^ |.q.| by A2, FINSEQ_2:10; :: thesis: verum