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 Th24, FINSEQ_1:2, TARSKI:def 1;
hence A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:87; :: thesis: <*<*a*>*> * (1,1) = a
( <*<*a*>*> . 1 = <*a*> & <*a*> . 1 = a ) by FINSEQ_1:40;
hence <*<*a*>*> * (1,1) = a by A1, Def5; :: thesis: verum