let D be non empty set ; :: thesis: for a, b, c, d being Element of D holds
( (a,b ][ c,d) * 1,1 = a & (a,b ][ c,d) * 1,2 = b & (a,b ][ c,d) * 2,1 = c & (a,b ][ c,d) * 2,2 = d )
let a, b, c, d be Element of D; :: thesis: ( (a,b ][ c,d) * 1,1 = a & (a,b ][ c,d) * 1,2 = b & (a,b ][ c,d) * 2,1 = c & (a,b ][ c,d) * 2,2 = d )
set M = a,b ][ c,d;
( (a,b ][ c,d) . 1 = <*a,b*> & (a,b ][ c,d) . 2 = <*c,d*> & <*a,b*> . 1 = a & <*a,b*> . 2 = b & <*c,d*> . 1 = c & <*c,d*> . 2 = d & [1,1] in Indices (a,b ][ c,d) & [1,2] in Indices (a,b ][ c,d) & [2,1] in Indices (a,b ][ c,d) & [2,2] in Indices (a,b ][ c,d) ) by Th4, FINSEQ_1:61;
hence ( (a,b ][ c,d) * 1,1 = a & (a,b ][ c,d) * 1,2 = b & (a,b ][ c,d) * 2,1 = c & (a,b ][ c,d) * 2,2 = d ) by MATRIX_1:def 6; :: thesis: verum