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

for AR being Subset of R holds (r * s) * AR = r * (s * AR)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R holds (r * s) * AR = r * (s * AR)

let AR be Subset of R; :: thesis: (r * s) * AR = r * (s * AR)

set rs = r * s;

assume x in r * (s * AR) ; :: thesis: x in (r * s) * AR

then consider v being Element of R such that

A2: x = r * v and

A3: v in s * AR ;

consider w being Element of R such that

A4: v = s * w and

A5: w in AR by A3;

(r * s) * w = x by A2, A4, RLVECT_1:def 7;

hence x in (r * s) * AR by A5; :: thesis: verum

for AR being Subset of R holds (r * s) * AR = r * (s * AR)

let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R holds (r * s) * AR = r * (s * AR)

let AR be Subset of R; :: thesis: (r * s) * AR = r * (s * AR)

set rs = r * s;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: r * (s * AR) c= (r * s) * AR

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (s * AR) or x in (r * s) * AR )let x be object ; :: thesis: ( x in (r * s) * AR implies x in r * (s * AR) )

assume x in (r * s) * AR ; :: thesis: x in r * (s * AR)

then consider v being Element of R such that

A1: ( x = (r * s) * v & v in AR ) ;

( s * v in s * AR & x = r * (s * v) ) by A1, RLVECT_1:def 7;

hence x in r * (s * AR) ; :: thesis: verum

end;assume x in (r * s) * AR ; :: thesis: x in r * (s * AR)

then consider v being Element of R such that

A1: ( x = (r * s) * v & v in AR ) ;

( s * v in s * AR & x = r * (s * v) ) by A1, RLVECT_1:def 7;

hence x in r * (s * AR) ; :: thesis: verum

assume x in r * (s * AR) ; :: thesis: x in (r * s) * AR

then consider v being Element of R such that

A2: x = r * v and

A3: v in s * AR ;

consider w being Element of R such that

A4: v = s * w and

A5: w in AR by A3;

(r * s) * w = x by A2, A4, RLVECT_1:def 7;

hence x in (r * s) * AR by A5; :: thesis: verum