let b, c, d, e, f, g, h, i be Real; :: thesis: for M being Matrix of 3,REAL st M = <*<*0,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = (((- ((c * e) * g)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
let M be Matrix of 3,REAL; :: thesis: ( M = <*<*0,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = (((- ((c * e) * g)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) )
assume M = <*<*0,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: Det M = (((- ((c * e) * g)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
then Det M = ((((((0 * e) * i) - ((c * e) * g)) - ((0 * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by Th1;
hence Det M = (((- ((c * e) * g)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) ; :: thesis: verum