let A be set ; :: thesis: for B, C being Element of Fin () holds B ^ C = C ^ B
let B, C be Element of Fin (); :: thesis: B ^ C = C ^ B
deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = \$1 \/ \$2;
defpred S1[ set , set ] means ( \$1 in B & \$2 in C );
defpred S2[ set , set ] means ( \$2 in C & \$1 in B );
set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ;
set X2 = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ;
A1: for s, t being Element of DISJOINT_PAIRS A holds H1(s,t) = H1(t,s) ;
A2: now :: thesis: for x being object holds
( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
let x be object ; :: thesis: ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex s, t being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
then ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex t, s being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
hence ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } ) ; :: thesis: verum
end;
A3: for s, t being Element of DISJOINT_PAIRS A holds
( S1[s,t] iff S2[s,t] ) ;
{ H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } from hence B ^ C = C ^ B by ; :: thesis: verum