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