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