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, Th3;
reconsider a = aa as Scalar of TernaryFieldEx ;
( Tern u,a,v = (uu * aa) + vv & Tern u9,a,v9 = (uu9 * aa) + vv9 ) by Def4;
hence ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u9,a,v9 by A2; :: thesis: verum