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