let a be Scalar of TernaryFieldEx; :: thesis: Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = a
reconsider x = a as Real ;
thus Tern (a,(1. TernaryFieldEx),(0. TernaryFieldEx)) = (x * jj) + zz by Def2
.= a ; :: thesis: verum