let F be Ternary-Field; :: thesis: for a, b, x, x9 being Scalar of F st a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) holds
x = x9
let a, b, x, x9 be Scalar of F; :: thesis: ( a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) implies x = x9 )
assume A1: ( a <> 0. F & Tern (x,a,b) = Tern (x9,a,b) ) ; :: thesis: x = x9
( Tern (x,(0. F),b) = b & Tern (x9,(0. F),b) = b ) by Def5;
hence x = x9 by A1, Def5; :: thesis: verum