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