theorem :: ALGSTR_3:2

for u, a, v being Scalar of TernaryFieldEx
for z, x, y being Real st u = z & a = x & v = y holds
Tern (u,a,v) = (z * x) + y by Def2;