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 Real ;
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 Def4; :: thesis: verum