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

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