let u, u' be Scalar of TernaryFieldEx ; :: thesis: ( u <> u' implies for v, v' being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v' )
assume A1: u <> u' ; :: thesis: for v, v' being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v'
let v, v' be Scalar of TernaryFieldEx ; :: thesis: ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v'
reconsider uu = u, uu' = u', vv = v, vv' = v' as Real ;
consider aa being Real such that
A2: (uu * aa) + vv = (uu' * aa) + vv' by A1, Th3;
reconsider a = aa as Scalar of TernaryFieldEx ;
( Tern u,a,v = (uu * aa) + vv & Tern u',a,v' = (uu' * aa) + vv' ) by Def4;
hence ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v' by A2; :: thesis: verum