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 set ; :: 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 set ; :: 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:121;
reconsider s9 = s, t9 = t as Function ;
( s is PartFunc of V,C & t is PartFunc of V,C ) by PARTFUN1:121;
then s9 +* t9 is PartFunc of V,C by FUNCT_4:41;
then s99 \/ t99 is PartFunc of V,C by A4, FUNCT_4:31;
hence y in PFuncs V,C by A3, PARTFUN1:119; :: 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