let D be non empty set ; :: thesis: for a being Element of D holds
( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * 1,1 = a )
let a be Element of D; :: thesis: ( [1,1] in Indices <*<*a*>*> & <*<*a*>*> * 1,1 = a )
set M = <*<*a*>*>;
( Indices <*<*a*>*> = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:4, MATRIX_1:25, TARSKI:def 1;
hence A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:106; :: thesis: <*<*a*>*> * 1,1 = a
( <*<*a*>*> . 1 = <*a*> & <*a*> . 1 = a ) by FINSEQ_1:57;
hence <*<*a*>*> * 1,1 = a by A1, MATRIX_1:def 6; :: thesis: verum