let r, s be Real; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
let L be Linear_Combination of V; :: thesis: r * (s (*) L) = s (*) (r * L)

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

suppose A1: s = 0 ; :: thesis: r * (s (*) L) = s (*) (r * L)

hence r * (s (*) L) = r * (ZeroLC V) by Def2
.= r * (0 * L) by RLVECT_2:43
.= (r * 0) * L by RLVECT_2:47
.= ZeroLC V by RLVECT_2:43
.= s (*) (r * L) by A1, Def2 ;
:: thesis: verum

end;

suppose A2: s <> 0 ; :: thesis: r * (s (*) L) = s (*) (r * L)

now :: thesis: for v being VECTOR of V holds (r * (s (*) L)) . v = (s (*) (r * L)) . v

let v be VECTOR of V; :: thesis: (r * (s (*) L)) . v = (s (*) (r * L)) . v
thus (r * (s (*) L)) . v = r * ((s (*) L) . v) by RLVECT_2:def 11
.= r * (L . ((s ") * v)) by A2, Def2
.= (r * L) . ((s ") * v) by RLVECT_2:def 11
.= (s (*) (r * L)) . v by A2, Def2 ; :: thesis: verum

end;

hence r * (s (*) L) = s (*) (r * L) ; :: thesis: verum

end;

end;