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

reconsider x = a as Real ;

thus Tern ((1. TernaryFieldEx),a,(0. TernaryFieldEx)) = ternaryreal . (jj,x,zz)

.= (x * 1) + 0 by Def2

.= a ; :: thesis: verum