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