let a, b be Scalar of TernaryFieldEx; :: thesis: Tern (a,(0. TernaryFieldEx),b) = b

reconsider x = a, y = b as Real ;

thus Tern (a,(0. TernaryFieldEx),b) = (x * 0) + y by Def2

.= b ; :: thesis: verum

reconsider x = a, y = b as Real ;

thus Tern (a,(0. TernaryFieldEx),b) = (x * 0) + y by Def2

.= b ; :: thesis: verum