let u,

a,

v,

v9 be

Scalar of

TernaryFieldEx;

( Tern (u,a,v) = Tern (u,a,v9) implies v = v9 )
reconsider z =

u,

x =

a,

y =

v,

y9 =

v9 as

Real ;

( Tern (

u,

a,

v)

= (z * x) + y &

Tern (

u,

a,

v9)

= (z * x) + y9 )

by Def2;

hence
( Tern (

u,

a,

v)

= Tern (

u,

a,

v9) implies

v = v9 )
;

verum