let F be Ternary-Field; :: thesis: for a, a9, u, u9, v, 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, u9, v, 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, Def5;

hence ( u = u9 & v = v9 ) by A2, Def5; :: thesis: verum

( u = u9 & v = v9 )

let a, a9, u, u9, v, 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, Def5;

hence ( u = u9 & v = v9 ) by A2, Def5; :: thesis: verum