let a, b be Scalar of TernaryFieldEx ; :: thesis: Tern (0. TernaryFieldEx ),a,b = b
reconsider x = a, y = b as Real ;
thus Tern (0. TernaryFieldEx ),a,b = (0 * x) + y by Def4
.= b ; :: thesis: verum