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;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: r * (s * AR) c= (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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (s * AR) or 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
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