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 Def4;
hence ( Tern u,a,v = Tern u,a,v9 implies v = v9 ) ; :: thesis: verum