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

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 )
;

end;

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

end;

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

hence
r (*) (ZeroLC R) = ZeroLC R
; :: thesis: verumlet 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;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