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

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

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

per cases ( n = 1 or n = 2 ) by A2, A4, FINSEQ_1:2, TARSKI:def 2;

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

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

end;

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

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

end;

end;

end;

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