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 (x,a,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 (x,a,b) = c )

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

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

consider x, z being Scalar of F such that

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

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

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

for b, c being Scalar of F ex x being Scalar of F st Tern (x,a,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 (x,a,b) = c )

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

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

consider x, z being Scalar of F such that

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

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

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