let V, C be set ; 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)); 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 for x being object holds
( 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 ) } )let x be
object ;
( 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 ) } )
;
verum end;
A2:
for s, t being Element of PFuncs (V,C) holds H1(s,t) = H1(t,s)
;
A3:
for s, t being Element of PFuncs (V,C) holds
( S1[s,t] iff S2[s,t] )
;
{ 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(A3, A2);
hence
A ^ B = B ^ A
by A1, TARSKI:2; verum