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*>*>;
A1: Indices <*<*a*>*> = [:(Seg 1),(Seg 1):] by MATRIX_1:25;
1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
hence A2: [1,1] in Indices <*<*a*>*> by A1, ZFMISC_1:106; :: thesis: <*<*a*>*> * 1,1 = a
( <*<*a*>*> . 1 = <*a*> & <*a*> . 1 = a ) by FINSEQ_1:57;
hence <*<*a*>*> * 1,1 = a by A2, MATRIX_1:def 6; :: thesis: verum