thus ( K is trivial implies 0. K = 1_ K ) ; :: thesis: ( 0. K = 1_ K implies K is trivial )
assume A1: 0. K = 1_ K ; :: thesis: K is trivial

now :: thesis: for x being Scalar of K holds x = 0. K

let x be Scalar of K; :: thesis: x = 0. K
thus x = x * (1_ K)
.= 0. K by A1 ; :: thesis: verum

end;

hence K is trivial ; :: thesis: verum