let V, C be set ; for A, B being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
let A, B be Element of Fin (PFuncs (V,C)); ( B = {{}} implies A ^ B = A )
A1:
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } c= A
A4:
A c= { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) }
proof
{} is
PartFunc of
V,
C
by RELSET_1:12;
then reconsider b =
{} as
Element of
PFuncs (
V,
C)
by PARTFUN1:45;
let a be
object ;
TARSKI:def 3 ( not a in A or a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } )
assume A5:
a in A
;
a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) }
A c= PFuncs (
V,
C)
by FINSUB_1:def 5;
then reconsider a9 =
a as
Element of
PFuncs (
V,
C)
by A5;
A6:
b in {{}}
by TARSKI:def 1;
(
a = a9 \/ b &
a9 tolerates b )
by PARTFUN1:59;
hence
a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) }
by A5, A6;
verum
end;
assume
B = {{}}
; A ^ B = A
hence
A ^ B = A
by A1, A4; verum