let a, b, c, d, e, f, g, h, i be Real; :: thesis: for M being Matrix of 3,REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
let M be Matrix of 3,REAL; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) )
assume A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
reconsider ra = a, rb = b, rc = c, rd = d, re = e, rf = f, rg = g, rh = h, ri = i as Element of F_Real by XREAL_0:def 1;
reconsider M1 = <*<*ra,rb,rc*>,<*rd,re,rf*>,<*rg,rh,ri*>*> as Matrix of 3,F_Real by MATRIXR2:35;
Det M1 = ((((((ra * re) * ri) - ((rc * re) * rg)) - ((ra * rf) * rh)) + ((rb * rf) * rg)) - ((rb * rd) * ri)) + ((rc * rd) * rh) by MATRIX_9:46;
hence Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by A1, MATRIXR1:def 1; :: thesis: verum