let a, b, c, d be set ; Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]}
thus Indices ((a,b) ][ (c,d)) =
[:(Seg 2),(Seg 2):]
by MATRIX_0:47
.=
[:{1},(Seg 2):] \/ [:{2},(Seg 2):]
by FINSEQ_1:2, ZFMISC_1:109
.=
[:{1},(Seg 2):] \/ {[2,1],[2,2]}
by FINSEQ_1:2, ZFMISC_1:30
.=
{[1,1],[1,2]} \/ {[2,1],[2,2]}
by FINSEQ_1:2, ZFMISC_1:30
.=
{[1,1],[1,2],[2,1],[2,2]}
by ENUMSET1:5
; verum