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 H₁( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S₁[ Function, Function] means ( $1 in A & $2 in B & $1 tolerates $2 );
defpred S₂[ Function, Function] means ( $2 in B & $1 in A & $2 tolerates $1 );
set X1 = { H₁(s,t) where s, t is Element of PFuncs (V,C) : S₁[s,t] } ;
set X2 = { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[s,t] } ;

A1: now :: thesis: for x being object holds
( x in { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[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 ; :: thesis: ( x in { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[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 { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[s,t] } iff ex s, t being Element of PFuncs (V,C) st
( x = H₁(t,s) & S₂[s,t] ) ) ;
then ( x in { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[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 { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[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 H₁(s,t) = H₁(t,s) ;
A3: for s, t being Element of PFuncs (V,C) holds
( S₁[s,t] iff S₂[s,t] ) ;
{ H₁(s,t) where s, t is Element of PFuncs (V,C) : S₁[s,t] } = { H₁(t,s) where s, t is Element of PFuncs (V,C) : S₂[s,t] } from FRAENKEL:sch 8(A3, A2);
hence A ^ B = B ^ A by A1, TARSKI:2; :: thesis: verum