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