let u, a, b be Scalar of TernaryFieldEx; :: thesis: ex v being Scalar of TernaryFieldEx st Tern (u,a,v) = b
reconsider z = u, x = a, y = b as Real ;
reconsider t = y - (z * x) as Element of REAL by XREAL_0:def 1;
reconsider v = t as Scalar of TernaryFieldEx ;
take v ; :: thesis: Tern (u,a,v) = b
y = (z * x) + t ;
hence Tern (u,a,v) = b by Def2; :: thesis: verum