let F be Ternary-Field; :: thesis: for a being Scalar of F st a <> 0. F holds

for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

let a be Scalar of F; :: thesis: ( a <> 0. F implies for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c )

assume A1: a <> 0. F ; :: thesis: for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

let b, c be Scalar of F; :: thesis: ex x being Scalar of F st Tern (a,x,b) = c

consider x being Scalar of F such that

A2: Tern (a,x,b) = Tern ((0. F),x,c) by A1, Def5;

take x ; :: thesis: Tern (a,x,b) = c

thus Tern (a,x,b) = c by A2, Def5; :: thesis: verum

for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

let a be Scalar of F; :: thesis: ( a <> 0. F implies for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c )

assume A1: a <> 0. F ; :: thesis: for b, c being Scalar of F ex x being Scalar of F st Tern (a,x,b) = c

let b, c be Scalar of F; :: thesis: ex x being Scalar of F st Tern (a,x,b) = c

consider x being Scalar of F such that

A2: Tern (a,x,b) = Tern ((0. F),x,c) by A1, Def5;

take x ; :: thesis: Tern (a,x,b) = c

thus Tern (a,x,b) = c by A2, Def5; :: thesis: verum