let V, C be set ; :: thesis: for B, A being Element of Fin (PFuncs V,C) st B = {{} } holds
A ^ B = A
let B, A 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 set ; :: 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:25;
then reconsider b = {} as Element of PFuncs V,C by PARTFUN1:119;
let a be set ; :: 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:141;
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, XBOOLE_0:def 10; :: thesis: verum