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