let r be Real; :: thesis: for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

let LR1, LR2 be Linear_Combination of R; :: thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

let LR1, LR2 be Linear_Combination of R; :: thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

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

end;

suppose A1:
r = 0
; :: thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

set Z = ZeroLC R;

.= (ZeroLC R) + (ZeroLC R) by A2

.= (r (*) LR1) + (ZeroLC R) by A1, Def2

.= (r (*) LR1) + (r (*) LR2) by A1, Def2 ; :: thesis: verum

end;A2: now :: thesis: for v being Element of R holds ((ZeroLC R) + (ZeroLC R)) . v = (ZeroLC R) . v

thus r (*) (LR1 + LR2) =
ZeroLC R
by A1, Def2
let v be Element of R; :: thesis: ((ZeroLC R) + (ZeroLC R)) . v = (ZeroLC R) . v

thus ((ZeroLC R) + (ZeroLC R)) . v = ((ZeroLC R) . v) + ((ZeroLC R) . v) by RLVECT_2:def 10

.= ((ZeroLC R) . v) + 0 by RLVECT_2:20

.= (ZeroLC R) . v ; :: thesis: verum

end;thus ((ZeroLC R) + (ZeroLC R)) . v = ((ZeroLC R) . v) + ((ZeroLC R) . v) by RLVECT_2:def 10

.= ((ZeroLC R) . v) + 0 by RLVECT_2:20

.= (ZeroLC R) . v ; :: thesis: verum

.= (ZeroLC R) + (ZeroLC R) by A2

.= (r (*) LR1) + (ZeroLC R) by A1, Def2

.= (r (*) LR1) + (r (*) LR2) by A1, Def2 ; :: thesis: verum

suppose A3:
r <> 0
; :: thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)

end;

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

hence
r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
; :: thesis: verumlet v be Element of R; :: thesis: (r (*) (LR1 + LR2)) . v = ((r (*) LR1) + (r (*) LR2)) . v

thus (r (*) (LR1 + LR2)) . v = (LR1 + LR2) . ((r ") * v) by A3, Def2

.= (LR1 . ((r ") * v)) + (LR2 . ((r ") * v)) by RLVECT_2:def 10

.= ((r (*) LR1) . v) + (LR2 . ((r ") * v)) by A3, Def2

.= ((r (*) LR1) . v) + ((r (*) LR2) . v) by A3, Def2

.= ((r (*) LR1) + (r (*) LR2)) . v by RLVECT_2:def 10 ; :: thesis: verum

end;thus (r (*) (LR1 + LR2)) . v = (LR1 + LR2) . ((r ") * v) by A3, Def2

.= (LR1 . ((r ") * v)) + (LR2 . ((r ") * v)) by RLVECT_2:def 10

.= ((r (*) LR1) . v) + (LR2 . ((r ") * v)) by A3, Def2

.= ((r (*) LR1) . v) + ((r (*) LR2) . v) by A3, Def2

.= ((r (*) LR1) + (r (*) LR2)) . v by RLVECT_2:def 10 ; :: thesis: verum