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

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