deffunc H1( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
set M = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
set N = { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } ;
A1:
{ H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } c= { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } or a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) } )
assume
a in { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) }
;
a in { H1(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 { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B ) }
;
verum
end;
A2:
{ H1(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 ;
TARSKI:def 3 ( not y in { H1(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 { H1(s,t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) }
;
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;
verum
end;
A5:
B is finite
;
A6:
A is finite
;
{ H1(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; verum