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 )
assume A1: B = {{} } ; :: thesis: A ^ B = A
{ (s \/ t) where s, t is Element of PFuncs V,C : ( s in A & t in {{} } & s tolerates t ) } = A

proof

thus { (s \/ t) where s, t is Element of PFuncs V,C : ( s in A & t in {{} } & s tolerates t ) } c= A :: according to XBOOLE_0:def 10 :: thesis: A c= { (s \/ t) where s, t is Element of PFuncs V,C : ( s in A & t in {{} } & s tolerates t ) }

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 s', t' being Element of PFuncs V,C such that
A2: ( a = s' \/ t' & s' in A & t' in {{} } & s' tolerates t' ) ;
t' = {} by A2, TARSKI:def 1;
hence a in A by A2; :: thesis: verum

end;

thus A c= { (s \/ t) where s, t is Element of PFuncs V,C : ( s in A & t in {{} } & s tolerates t ) } :: thesis: verum

proof

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 ) } )
A3: A c= PFuncs V,C by FINSUB_1:def 5;
assume A4: 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 ) }
then reconsider a' = a as Element of PFuncs V,C by A3;
{} is PartFunc of V,C by RELSET_1:25;
then reconsider b = {} as Element of PFuncs V,C by PARTFUN1:119;
A5: a = a' \/ b ;
A6: a' tolerates b by PARTFUN1:141;
b in {{} } by TARSKI:def 1;
hence a in { (s \/ t) where s, t is Element of PFuncs V,C : ( s in A & t in {{} } & s tolerates t ) } by A4, A5, A6; :: thesis: verum

end;

end;

hence A ^ B = A by A1; :: thesis: verum