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