let a, b, c, d, e be Real; :: thesis: |{|[a,1,0]|,|[b,0,1]|,|[c,d,e]|}| = (c - (a * d)) - (e * b)
reconsider p = |[a,1,0]|, q = |[b,0,1]|, r = |[c,d,e]| as Element of (TOP-REAL 3) ;
A1: ( p `1 = a & p `2 = 1 & p `3 = 0 & q `1 = b & q `2 = 0 & q `3 = 1 & r `1 = c & r `2 = d & r `3 = e ) by EUCLID_5:2;
|{|[a,1,0]|,|[b,0,1]|,|[c,d,e]|}| = (((((((p `1) * (q `2)) * (r `3)) - (((p `3) * (q `2)) * (r `1))) - (((p `1) * (q `3)) * (r `2))) + (((p `2) * (q `3)) * (r `1))) - (((p `2) * (q `1)) * (r `3))) + (((p `3) * (q `1)) * (r `2)) by ANPROJ_8:27;
hence |{|[a,1,0]|,|[b,0,1]|,|[c,d,e]|}| = (c - (a * d)) - (e * b) by A1; :: thesis: verum