deffunc H₁( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
set M = { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
set N = { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ;
A1: { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or a in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } )
assume a in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; :: thesis: a in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }
then ex s, t being Element of PFuncs (V,C) st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence a in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ; :: thesis: verum

end;

A2: { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= PFuncs (V,C)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or y in PFuncs (V,C) )
assume y in { H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ; :: thesis: y in PFuncs (V,C)
then consider s, t being Element of PFuncs (V,C) such that
A3: y = s \/ t and
s in A and
t in B and
A4: s tolerates t ;
reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47;
reconsider s9 = s, t9 = t as Function ;
( s is PartFunc of V,C & t is PartFunc of V,C ) by PARTFUN1:47;
then s9 +* t9 is PartFunc of V,C by FUNCT_4:40;
then s99 \/ t99 is PartFunc of V,C by A4, FUNCT_4:30;
hence y in PFuncs (V,C) by A3, PARTFUN1:45; :: thesis: verum

end;

A5: B is finite ;
A6: A is finite ;
{ H₁(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } is finite from FRAENKEL:sch 22(A6, A5);
hence { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def 5; :: thesis: verum