let u, u9 be Scalar of TernaryFieldEx; :: thesis: ( u <> u9 implies for v, v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) )
assume A1: u <> u9 ; :: thesis: for v, v9 being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9)
let v, v9 be Scalar of TernaryFieldEx; :: thesis: ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9)
reconsider uu = u, uu9 = u9, vv = v, vv9 = v9 as Real ;
consider aa being Real such that
A2: (uu * aa) + vv = (uu9 * aa) + vv9 by A1, Th1;
reconsider a = aa as Scalar of TernaryFieldEx by XREAL_0:def 1;
( Tern (u,a,v) = (uu * aa) + vv & Tern (u9,a,v9) = (uu9 * aa) + vv9 ) by Def2;
hence ex a being Scalar of TernaryFieldEx st Tern (u,a,v) = Tern (u9,a,v9) by A2; :: thesis: verum