let x, y be Complex; |.<*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 for n being Nat st n in dom |.<*x,y*>.| holds
|.<*x,y*>.| . n = <*|.x.|,|.y.|*> . nlet n be
Nat;
( n in dom |.<*x,y*>.| implies |.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1 )assume A4:
n in dom |.<*x,y*>.|
;
|.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1per cases
( n = 1 or n = 2 )
by A2, A4, FINSEQ_1:2, TARSKI:def 2;
suppose A5:
n = 1
;
|.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1then 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.|
by FINSEQ_1:44;
hence
|.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n
by A5, FINSEQ_1:44;
verum end; suppose A7:
n = 2
;
|.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1then 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.|
by FINSEQ_1:44;
hence
|.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n
by A7, FINSEQ_1:44;
verum end; end; end;
len <*|.x.|,|.y.|*> = 2
by FINSEQ_1:44;
hence
|.<*x,y*>.| = <*|.x.|,|.y.|*>
by A1, A3, FINSEQ_2:9; verum