let V, C be set ; :: thesis: 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)); :: thesis: ( 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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } or a in A )
assume a in { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in {{}} & s tolerates t ) } ; :: thesis: a in A
then consider s9, t9 being Element of PFuncs (V,C) such that
A2: ( a = s9 \/ t9 & s9 in A ) and
A3: t9 in {{}} and
s9 tolerates t9 ;
t9 = {} by A3, TARSKI:def 1;
hence a in A by A2; :: thesis: verum

end;

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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

assume B = {{}} ; :: thesis: A ^ B = A
hence A ^ B = A by A1, A4; :: thesis: verum