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 ;
A2: now :: thesis: for a being Vector of V holds a = 0. V
let a be Vector of V; :: thesis: a = 0. V
thus a = (1_ K) * a by VECTSP_1:def 17
.= 0. V by A1, VECTSP_1:14 ; :: thesis: verum
end;
now :: thesis: for r being Scalar of K holds r = 0. K
let r be Scalar of K; :: thesis: r = 0. K
thus r = r * (1_ K)
.= 0. K by A1 ; :: 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