let D be non empty set ; for x being Element of D holds <*<*x*>*> = <*<*x*>*> @
let x be Element of D; <*<*x*>*> = <*<*x*>*> @
set P = <*<*x*>*>;
set R = <*<*x*>*> @ ;
A1:
len <*<*x*>*> = 1
by FINSEQ_1:40;
then A2: width <*<*x*>*> =
len <*x*>
by MATRIX_0:20
.=
1
by FINSEQ_1:40
;
then A3:
len (<*<*x*>*> @) = 1
by MATRIX_0:54;
A4:
now for i, j being Nat st [i,j] in Indices <*<*x*>*> holds
<*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j)let i,
j be
Nat;
( [i,j] in Indices <*<*x*>*> implies <*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j) )assume A5:
[i,j] in Indices <*<*x*>*>
;
<*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j)then A6:
[i,j] in [:(dom <*<*x*>*>),(Seg 1):]
by A2, MATRIX_0:def 4;
then
i in dom <*<*x*>*>
by ZFMISC_1:87;
then
i in Seg 1
by A1, FINSEQ_1:def 3;
then A7:
i = 1
by FINSEQ_1:2, TARSKI:def 1;
j in Seg 1
by A6, ZFMISC_1:87;
then
j = 1
by FINSEQ_1:2, TARSKI:def 1;
hence
<*<*x*>*> * (
i,
j)
= (<*<*x*>*> @) * (
i,
j)
by A5, A7, MATRIX_0:def 6;
verum end;
width (<*<*x*>*> @) = 1
by A1, A2, MATRIX_0:54;
hence
<*<*x*>*> = <*<*x*>*> @
by A1, A2, A3, A4, MATRIX_0:21; verum