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

x = x9

let a, b, x, x9 be Scalar of F; :: thesis: ( a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) implies x = x9 )

assume that

A1: a <> 0. F and

A2: Tern (a,x,b) = Tern (a,x9,b) ; :: thesis: x = x9

set c = Tern (a,x,b);

A3: Tern (a,x,b) = Tern ((0. F),x,(Tern (a,x,b))) by Def5;

Tern (a,x9,b) = Tern ((0. F),x9,(Tern (a,x,b))) by A2, Def5;

hence x = x9 by A1, A3, Def5; :: thesis: verum

x = x9

let a, b, x, x9 be Scalar of F; :: thesis: ( a <> 0. F & Tern (a,x,b) = Tern (a,x9,b) implies x = x9 )

assume that

A1: a <> 0. F and

A2: Tern (a,x,b) = Tern (a,x9,b) ; :: thesis: x = x9

set c = Tern (a,x,b);

A3: Tern (a,x,b) = Tern ((0. F),x,(Tern (a,x,b))) by Def5;

Tern (a,x9,b) = Tern ((0. F),x9,(Tern (a,x,b))) by A2, Def5;

hence x = x9 by A1, A3, Def5; :: thesis: verum