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:44;
A2: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:44;
A3: ( [2,1] in Indices ((a,b) ][ (c,d)) & [2,2] in Indices ((a,b) ][ (c,d)) ) by Th48;
A4: ( <*c,d*> . 1 = c & <*c,d*> . 2 = d ) by FINSEQ_1:44;
( [1,1] in Indices ((a,b) ][ (c,d)) & [1,2] in Indices ((a,b) ][ (c,d)) ) by Th48;
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, Def5; :: thesis: verum