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