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