let K be Ring; :: thesis: for V being LeftMod of K st K is trivial holds
( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
let V be LeftMod of K; :: thesis: ( K is trivial implies ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) ) )
assume K is trivial ; :: thesis: ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) )
then A1: 0. K = 1_ K by Def2;

A2: now

let a be Vector of V; :: thesis: a = 0. V
thus a = (1_ K) * a by VECTSP_1:def 29
.= 0. V by A1, VECTSP_1:59 ; :: thesis: verum

end;

now

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

end;

hence ( ( for r being Scalar of K holds r = 0. K ) & ( for a being Vector of V holds a = 0. V ) ) by A2; :: thesis: verum