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