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)

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

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

set Z = ZeroLC R;

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

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 r (*) (LR1 + LR2) = ZeroLC R by A1, Def2
.= (ZeroLC R) + (ZeroLC R) by A2
.= (r (*) LR1) + (ZeroLC R) by A1, Def2
.= (r (*) LR1) + (r (*) LR2) by A1, Def2 ; :: thesis: verum

end;

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

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

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

hence r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2) ; :: thesis: verum

end;

end;