let D be non empty set ; :: thesis: for x being Element of D holds <*<*x*>*> = <*<*x*>*> @
let x be Element of D; :: thesis: <*<*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 :: thesis: for i, j being Nat st [i,j] in Indices <*<*x*>*> holds
<*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices <*<*x*>*> implies <*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j) )
assume A5: [i,j] in Indices <*<*x*>*> ; :: thesis: <*<*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; :: thesis: verum

end;

width (<*<*x*>*> @) = 1 by A1, A2, MATRIX_0:54;
hence <*<*x*>*> = <*<*x*>*> @ by A1, A2, A3, A4, MATRIX_0:21; :: thesis: verum