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

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

end;

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