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 ;
A1: Tern u,a,v = (z * x) + y by Def4;
Tern u,a,v' = (z * x) + y' by Def4;
hence ( Tern u,a,v = Tern u,a,v' implies v = v' ) by A1; :: thesis: verum