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_2:3
.=
[:{1},(Seg 2):] \/ [:{2},(Seg 2):]
by FINSEQ_1:4, ZFMISC_1:132
.=
[:{1},(Seg 2):] \/ {[2,1],[2,2]}
by FINSEQ_1:4, ZFMISC_1:36
.=
{[1,1],[1,2]} \/ {[2,1],[2,2]}
by FINSEQ_1:4, ZFMISC_1:36
.=
{[1,1],[1,2],[2,1],[2,2]}
by ENUMSET1:45
; verum