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)) = ternaryreal . (jj,x,zz)
.= (x * 1) + 0 by Def2
.= a ; :: thesis: verum