let x1, x2, y1, y2 be object ; :: thesis: ( [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; :: thesis: verum