let a, a9 be Scalar of TernaryFieldEx; :: thesis: ( a <> a9 implies for b, b9 being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 ) )

assume A1: a <> a9 ; :: thesis: for b, b9 being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

let b, b9 be Scalar of TernaryFieldEx; :: thesis: ex u, v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

reconsider x = a, x9 = a9, y = b, y9 = b9 as Real ;

A2: x9 - x <> 0 by A1;

set s = (y9 - y) / (x9 - x);

set t = y - (x * ((y9 - y) / (x9 - x)));

reconsider u = (y9 - y) / (x9 - x), v = y - (x * ((y9 - y) / (x9 - x))) as Scalar of TernaryFieldEx by XREAL_0:def 1;

take u ; :: thesis: ex v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

take v ; :: thesis: ( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

thus Tern (u,a,v) = (((y9 - y) / (x9 - x)) * x) + ((- (((y9 - y) / (x9 - x)) * x)) + y) by Def2

.= b ; :: thesis: Tern (u,a9,v) = b9

thus Tern (u,a9,v) = (((y9 - y) / (x9 - x)) * x9) + ((- (x * ((y9 - y) / (x9 - x)))) + y) by Def2

.= (((y9 - y) / (x9 - x)) * (x9 - x)) + y

.= (y9 - y) + y by A2, XCMPLX_1:87

.= b9 ; :: thesis: verum

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 ) )

assume A1: a <> a9 ; :: thesis: for b, b9 being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

let b, b9 be Scalar of TernaryFieldEx; :: thesis: ex u, v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

reconsider x = a, x9 = a9, y = b, y9 = b9 as Real ;

A2: x9 - x <> 0 by A1;

set s = (y9 - y) / (x9 - x);

set t = y - (x * ((y9 - y) / (x9 - x)));

reconsider u = (y9 - y) / (x9 - x), v = y - (x * ((y9 - y) / (x9 - x))) as Scalar of TernaryFieldEx by XREAL_0:def 1;

take u ; :: thesis: ex v being Scalar of TernaryFieldEx st

( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

take v ; :: thesis: ( Tern (u,a,v) = b & Tern (u,a9,v) = b9 )

thus Tern (u,a,v) = (((y9 - y) / (x9 - x)) * x) + ((- (((y9 - y) / (x9 - x)) * x)) + y) by Def2

.= b ; :: thesis: Tern (u,a9,v) = b9

thus Tern (u,a9,v) = (((y9 - y) / (x9 - x)) * x9) + ((- (x * ((y9 - y) / (x9 - x)))) + y) by Def2

.= (((y9 - y) / (x9 - x)) * (x9 - x)) + y

.= (y9 - y) + y by A2, XCMPLX_1:87

.= b9 ; :: thesis: verum