let x, y, z be Complex; :: thesis: |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
A1: len |.<*x,y,z*>.| = len <*x,y,z*> by Def2
.= 3 by FINSEQ_1:45 ;
then A2: dom |.<*x,y,z*>.| = Seg 3 by FINSEQ_1:def 3;

A3: now :: thesis: for n being Nat st n in dom |.<*x,y,z*>.| holds
|.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n

let n be Nat; :: thesis: ( n in dom |.<*x,y,z*>.| implies |.<*x,y,z*>.| . b₁ = <*|.x.|,|.y.|,|.z.|*> . b₁ )
assume A4: n in dom |.<*x,y,z*>.| ; :: thesis: |.<*x,y,z*>.| . b₁ = <*|.x.|,|.y.|,|.z.|*> . b₁

per cases ( n = 1 or n = 2 or n = 3 ) by A2, A4, ENUMSET1:def 1, FINSEQ_3:1;

suppose A5: n = 1 ; :: thesis: |.<*x,y,z*>.| . b₁ = <*|.x.|,|.y.|,|.z.|*> . b₁

A6: 1 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.| . 1 = |.(<*x,y,z*> . 1).| by A6, Def2;
then |.<*x,y,z*>.| . 1 = |.x.| ;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A5; :: thesis: verum

end;

suppose A7: n = 2 ; :: thesis: |.<*x,y,z*>.| . b₁ = <*|.x.|,|.y.|,|.z.|*> . b₁

A8: 2 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.| . 2 = |.(<*x,y,z*> . 2).| by A8, Def2;
then |.<*x,y,z*>.| . 2 = |.y.| ;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A7; :: thesis: verum

end;

suppose A9: n = 3 ; :: thesis: |.<*x,y,z*>.| . b₁ = <*|.x.|,|.y.|,|.z.|*> . b₁

A10: 3 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.| . 3 = |.(<*x,y,z*> . 3).| by A10, Def2;
then |.<*x,y,z*>.| . 3 = |.z.| ;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A9; :: thesis: verum

end;

end;

end;

len <*|.x.|,|.y.|,|.z.|*> = 3 by FINSEQ_1:45;
hence |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*> by A1, A3, FINSEQ_2:9; :: thesis: verum