let F be Ternary-Field; :: thesis: for a, a9, u, v, u9, v9 being Scalar of F st a <> a9 & Tern u,a,v = Tern u9,a,v9 & Tern u,a9,v = Tern u9,a9,v9 holds
( u = u9 & v = v9 )
let a, a9, u, v, u9, v9 be Scalar of F; :: thesis: ( a <> a9 & Tern u,a,v = Tern u9,a,v9 & Tern u,a9,v = Tern u9,a9,v9 implies ( u = u9 & v = v9 ) )
assume that
A1: a <> a9 and
A2: Tern u,a,v = Tern u9,a,v9 and
A3: Tern u,a9,v = Tern u9,a9,v9 ; :: thesis: ( u = u9 & v = v9 )
u = u9 by A1, A2, A3, Def7;
hence ( u = u9 & v = v9 ) by A2, Def7; :: thesis: verum