now :: thesis: for I, J being Subset of R holds I *' J = J *' I

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

A1: now :: thesis: for u being object st u in J *' I holds
u in I *' J

let u be object ; :: 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
A2: u = Sum s and
A3: 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 ex a, b being Element of R st
( s . i = a * b & a in J & b in I ) by A3;
hence ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) ; :: thesis: verum

end;

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

end;

now :: thesis: for u being object st u in I *' J holds
u in J *' I

let u be object ; :: 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
A4: u = Sum s and
A5: 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 ex a, b being Element of R st
( s . i = a * b & a in I & b in J ) by A5;
hence ex a, b being Element of R st
( s . i = a * b & a in J & b in I ) ; :: thesis: verum

end;

hence u in J *' I 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