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