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

A3: now

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 TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 1 in dom |.<*x,y,z*>.| by A6, FINSEQ_3:31;
then |.<*x,y,z*>.| . 1 = |.<*x,y,z*>.| /. 1 by PARTFUN1:def 8
.= |.(<*x,y,z*> /. 1).| by A6, Def1 ;
then |.<*x,y,z*>.| . 1 = |.x.| by FINSEQ_4:27;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A5, FINSEQ_1:62; :: thesis: verum

end;

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

A8: 2 in dom <*x,y,z*> by TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 2 in dom |.<*x,y,z*>.| by A8, FINSEQ_3:31;
then |.<*x,y,z*>.| . 2 = |.<*x,y,z*>.| /. 2 by PARTFUN1:def 8
.= |.(<*x,y,z*> /. 2).| by A8, Def1 ;
then |.<*x,y,z*>.| . 2 = |.y.| by FINSEQ_4:27;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A7, FINSEQ_1:62; :: thesis: verum

end;

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

A10: 3 in dom <*x,y,z*> by TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 3 in dom |.<*x,y,z*>.| by A10, FINSEQ_3:31;
then |.<*x,y,z*>.| . 3 = |.<*x,y,z*>.| /. 3 by PARTFUN1:def 8
.= |.(<*x,y,z*> /. 3).| by A10, Def1 ;
then |.<*x,y,z*>.| . 3 = |.z.| by FINSEQ_4:27;
hence |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A9, FINSEQ_1:62; :: thesis: verum

end;

end;

end;

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