let F be Ternary-Field; :: thesis: for a, x, b, x' being Scalar of F st a <> 0. F & Tern a,x,b = Tern a,x',b holds
x = x'
let a, x, b, x' be Scalar of F; :: thesis: ( a <> 0. F & Tern a,x,b = Tern a,x',b implies x = x' )
assume that
A1: a <> 0. F and
A2: Tern a,x,b = Tern a,x',b ; :: thesis: x = x'
set c = Tern a,x,b;
A3: Tern a,x,b = Tern (0. F),x,(Tern a,x,b) by Def7;
Tern a,x',b = Tern (0. F),x',(Tern a,x,b) by A2, Def7;
hence x = x' by A1, A3, Def7; :: thesis: verum