let a, b, c, d, e be Real; :: thesis: |{|[1,0,a]|,|[0,1,b]|,|[c,d,e]|}| = (e - (c * a)) - (d * b)
reconsider p = |[1,0,a]|, q = |[0,1,b]|, r = |[c,d,e]| as Element of (TOP-REAL 3) ;
|{|[1,0,a]|,|[0,1,b]|,|[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 |{|[1,0,a]|,|[0,1,b]|,|[c,d,e]|}| = (e - (c * a)) - (d * b) ; :: thesis: verum