let u, a, v, v9 be Scalar of TernaryFieldEx; :: thesis: ( Tern (u,a,v) = Tern (u,a,v9) implies v = v9 )
reconsider z = u, x = a, y = v, y9 = v9 as Real ;
( Tern (u,a,v) = (z * x) + y & Tern (u,a,v9) = (z * x) + y9 ) by Def2;
hence ( Tern (u,a,v) = Tern (u,a,v9) implies v = v9 ) ; :: thesis: verum