let r be Real; :: thesis: for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds r (*) (ZeroLC R) = ZeroLC R
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: r (*) (ZeroLC R) = ZeroLC R

per cases ( r = 0 or r <> 0 ) ;

suppose r = 0 ; :: thesis: r (*) (ZeroLC R) = ZeroLC R

hence r (*) (ZeroLC R) = ZeroLC R by Def2; :: thesis: verum

end;

suppose A1: r <> 0 ; :: thesis: r (*) (ZeroLC R) = ZeroLC R

now :: thesis: for v being Element of R holds (r (*) (ZeroLC R)) . v = (ZeroLC R) . v

let v be Element of R; :: thesis: (r (*) (ZeroLC R)) . v = (ZeroLC R) . v
thus (r (*) (ZeroLC R)) . v = (ZeroLC R) . ((r ") * v) by A1, Def2
.= 0 by RLVECT_2:20
.= (ZeroLC R) . v by RLVECT_2:20 ; :: thesis: verum

end;

hence r (*) (ZeroLC R) = ZeroLC R ; :: thesis: verum

end;

end;