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

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 A5: n = 1 by X, FINSEQ_1:4, TARSKI:def 1;
hence |.<*x*>.| . n = |.<*x*>.| /. 1 by A4, PARTFUN1:def 8
.= |.(<*x*> /. 1).| by A3, Def1
.= |.x.| by FINSEQ_4:25
.= <*|.x.|*> . n by A5, FINSEQ_1:57 ;
:: thesis: verum

end;

hence |.<*x*>.| = <*|.x.|*> by A1, A2, FINSEQ_2:10; :: thesis: verum