let x be Complex; :: thesis: |.<*x*>.| = <*|.x.|*>
0 + 1 in Seg (0 + 1) by FINSEQ_1:4;
then A1: 1 in dom <*x*> by FINSEQ_1:38;
A2: len |.<*x*>.| = len <*x*> by Def2
.= 1 by FINSEQ_1:39 ;
then A3: dom |.<*x*>.| = Seg 1 by FINSEQ_1:def 3;

A5: now :: thesis: for n being Nat st n in dom |.<*x*>.| holds
|.<*x*>.| . n = <*|.x.|*> . n

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:2, TARSKI:def 1;
hence |.<*x*>.| . n = |.(<*x*> . 1).| by A1, Def2
.= |.x.|
.= <*|.x.|*> . n by A6 ;
:: thesis: verum

end;

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