now

let I, J be Subset of R; :: thesis: I *' J = J *' I

A1: now

let u be set ; :: thesis: ( u in I *' J implies u in J *' I )
assume u in I *' J ; :: thesis: u in J *' I
then consider s being FinSequence of the carrier of R such that
A2: ( u = Sum s & ( for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) ) ) ;
for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in J & b in I )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len s implies ex a, b being Element of R st
( s . i = a * b & a in J & b in I ) )
assume ( 1 <= i & i <= len s ) ; :: thesis: ex a, b being Element of R st
( s . i = a * b & a in J & b in I )
then consider a, b being Element of R such that
A3: ( s . i = a * b & a in I & b in J ) by A2;
thus ex a, b being Element of R st
( s . i = a * b & a in J & b in I ) by A3; :: thesis: verum

end;

hence u in J *' I by A2; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in J *' I implies u in I *' J )
assume u in J *' I ; :: thesis: u in I *' J
then consider s being FinSequence of the carrier of R such that
A4: ( u = Sum s & ( for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in J & b in I ) ) ) ;
for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in I & b in J )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len s implies ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) )
assume ( 1 <= i & i <= len s ) ; :: thesis: ex a, b being Element of R st
( s . i = a * b & a in I & b in J )
then consider a, b being Element of R such that
A5: ( s . i = a * b & a in J & b in I ) by A4;
thus ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) by A5; :: thesis: verum

end;

hence u in I *' J by A4; :: thesis: verum

end;

hence I *' J = J *' I by A1, TARSKI:2; :: thesis: verum

end;

hence for I, J being Subset of R holds I *' J = J *' I ; :: thesis: verum