let L be non empty ZeroOneStr ; :: thesis: 1. (L,1) = <*<*(1. L)*>*>
( Indices (1. (L,1)) = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:2, MATRIX_0:24, TARSKI:def 1;
then [1,1] in Indices (1. (L,1)) by ZFMISC_1:87;
then (1. (L,1)) * (1,1) = 1. L by MATRIX_1:def 3;
hence 1. (L,1) = <*<*(1. L)*>*> by Th33; :: thesis: verum