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

now

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

end;

hence K is trivial by STRUCT_0:def 19; :: thesis: verum