let a, b, c, d, e, f, g, h, i be Element of F_Real; :: thesis: for M being Matrix of 3,F_Real st a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = g - i
let M be Matrix of 3,F_Real; :: thesis: ( a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = g - i )
assume that
A1: ( a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 ) and
A2: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: Det M = g - i
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by A2, MATRIX_9:46
.= g - i by A1 ;
hence Det M = g - i ; :: thesis: verum