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;
A1: ( (a,b ][ c,d) . 1 = <*a,b*> & (a,b ][ c,d) . 2 = <*c,d*> ) by FINSEQ_1:61;
A2: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:61;
A3: ( [2,1] in Indices (a,b ][ c,d) & [2,2] in Indices (a,b ][ c,d) ) by Th4;
A4: ( <*c,d*> . 1 = c & <*c,d*> . 2 = d ) by FINSEQ_1:61;
( [1,1] in Indices (a,b ][ c,d) & [1,2] in Indices (a,b ][ c,d) ) by Th4;
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 A1, A2, A4, A3, MATRIX_1:def 6; :: thesis: verum