let a, a9, u, u9, v, v9 be Scalar of TernaryFieldEx; :: thesis: ( Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 implies u = u9 )
assume A1: ( Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) ) ; :: thesis: ( a = a9 or u = u9 )
reconsider aa = a, aa9 = a9, uu = u, uu9 = u9, vv = v, vv9 = v9 as Real ;
A2: ( Tern (u,a9,v) = (uu * aa9) + vv & Tern (u9,a9,v9) = (uu9 * aa9) + vv9 ) by Def2;
( Tern (u,a,v) = (uu * aa) + vv & Tern (u9,a,v9) = (uu9 * aa) + vv9 ) by Def2;
then uu * (aa - aa9) = uu9 * (aa - aa9) by A1, A2;
then ( uu = uu9 or aa - aa9 = 0 ) by XCMPLX_1:5;
hence ( a = a9 or u = u9 ) ; :: thesis: verum