let x be Element of F_Complex ; :: thesis: |.<*x*>.| = <*|.x.|*>
0 + 1 in Seg (0 + 1) by FINSEQ_1:6;
then A1: 1 in dom <*x*> by FINSEQ_1:55;
A2: len |.<*x*>.| = len <*x*> by Def1
.= 1 by FINSEQ_1:56 ;
then A3: dom |.<*x*>.| = Seg 1 by FINSEQ_1:def 3;
len |.<*x*>.| = len <*x*> by Def1;
then A4: 1 in dom |.<*x*>.| by A1, FINSEQ_3:31;

A5: now

let n be Nat; :: thesis: ( n in dom |.<*x*>.| implies |.<*x*>.| . n = <*|.x.|*> . n )
assume n in dom |.<*x*>.| ; :: thesis: |.<*x*>.| . n = <*|.x.|*> . n
then A6: n = 1 by A3, FINSEQ_1:4, TARSKI:def 1;
hence |.<*x*>.| . n = |.<*x*>.| /. 1 by A4, PARTFUN1:def 8
.= |.(<*x*> /. 1).| by A1, Def1
.= |.x.| by FINSEQ_4:25
.= <*|.x.|*> . n by A6, FINSEQ_1:57 ;
:: thesis: verum

end;

len <*|.x.|*> = 1 by FINSEQ_1:56;
hence |.<*x*>.| = <*|.x.|*> by A2, A5, FINSEQ_2:10; :: thesis: verum