let x, y be Element of F_Complex ; :: thesis: |.<*x,y*>.| = <*|.x.|,|.y.|*>
A1: len |.<*x,y*>.| = len <*x,y*> by Def1
.= 2 by FINSEQ_1:61 ;
then A2: dom |.<*x,y*>.| = Seg 2 by FINSEQ_1:def 3;

A3: now

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:4, 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_3:29;
|.<*x,y*>.| . 1 = |.<*x,y*>.| /. 1 by A4, A5, PARTFUN1:def 8
.= |.(<*x,y*> /. 1).| by A6, Def1 ;
then |.<*x,y*>.| . 1 = |.x.| by FINSEQ_4:26;
hence |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A5, FINSEQ_1:61; :: 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_3:29;
|.<*x,y*>.| . 2 = |.<*x,y*>.| /. 2 by A4, A7, PARTFUN1:def 8
.= |.(<*x,y*> /. 2).| by A8, Def1 ;
then |.<*x,y*>.| . 2 = |.y.| by FINSEQ_4:26;
hence |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A7, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

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