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 ;
A2: len <*|.x.|,|.y.|*> = 2 by FINSEQ_1:61;
X: dom |.<*x,y*>.| = Seg 2 by A1, FINSEQ_1:def 3;

now

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

per cases ( n = 1 or n = 2 ) by A3, X, FINSEQ_1:4, TARSKI:def 2;

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

then A5: 1 in dom <*x,y*> by A3, X, FINSEQ_3:29;
len |.<*x,y*>.| = len <*x,y*> by Def1;
then 1 in dom |.<*x,y*>.| by A5, FINSEQ_3:31;
then |.<*x,y*>.| . 1 = |.<*x,y*>.| /. 1 by PARTFUN1:def 8
.= |.(<*x,y*> /. 1).| by A5, Def1 ;
then |.<*x,y*>.| . 1 = |.x.| by FINSEQ_4:26;
hence |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A4, FINSEQ_1:61; :: thesis: verum

end;

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

then A7: 2 in dom <*x,y*> by A3, X, FINSEQ_3:29;
len |.<*x,y*>.| = len <*x,y*> by Def1;
then 2 in dom |.<*x,y*>.| by A7, FINSEQ_3:31;
then |.<*x,y*>.| . 2 = |.<*x,y*>.| /. 2 by PARTFUN1:def 8
.= |.(<*x,y*> /. 2).| by A7, Def1 ;
then |.<*x,y*>.| . 2 = |.y.| by FINSEQ_4:26;
hence |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A6, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

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