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:57;
then A2: width <*<*x*>*> = len <*x*> by MATRIX_1:20
.= 1 by FINSEQ_1:57 ;
then A3: len (<*<*x*>*> @ ) = 1 by MATRIX_2:12;
A4: width (<*<*x*>*> @ ) = 1 by A1, A2, MATRIX_2:12;

now

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 [i,j] in [:(dom <*<*x*>*>),(Seg 1):] by A2, MATRIX_1:def 5;
then ( i in dom <*<*x*>*> & j in Seg 1 ) by ZFMISC_1:106;
then ( i in Seg 1 & j in Seg 1 ) by A1, FINSEQ_1:def 3;
then ( i = 1 & j = 1 ) by FINSEQ_1:4, TARSKI:def 1;
hence <*<*x*>*> * i,j = (<*<*x*>*> @ ) * i,j by A5, MATRIX_1:def 7; :: thesis: verum

end;

hence <*<*x*>*> = <*<*x*>*> @ by A1, A2, A3, A4, MATRIX_1:21; :: thesis: verum