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;

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

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)

width (<*<*x*>*> @) = 1
by A1, A2, MATRIX_0:54;<*<*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;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

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