let x1, x2, y1, y2 be object ; ( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )
A1:
2 in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
( Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] & 1 in Seg 2 )
by Th47, FINSEQ_1:2, TARSKI:def 2;
hence
( [1,1] in Indices ((x1,x2) ][ (y1,y2)) & [1,2] in Indices ((x1,x2) ][ (y1,y2)) & [2,1] in Indices ((x1,x2) ][ (y1,y2)) & [2,2] in Indices ((x1,x2) ][ (y1,y2)) )
by A1, ZFMISC_1:87; verum