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

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