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 * 1) + 0 by Def4
.= a ; :: thesis: verum