let V, C be set ; :: thesis: for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
let B be Element of Fin (PFuncs (V,C)); :: thesis: B c= B ^ B

now :: thesis: for a being set st a in B holds
a in B ^ B

let a be set ; :: thesis: ( a in B implies a in B ^ B )
assume A1: a in B ; :: thesis: a in B ^ B
B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
( a = a \/ a & a9 tolerates a9 ) ;
hence a in B ^ B by A1; :: thesis: verum

end;

hence B c= B ^ B ; :: thesis: verum