let V, C be set ; :: thesis: for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
let A be Element of Fin (PFuncs (V,C)); :: thesis: mi A c= A
for a being set st a in mi A holds
a in A by Th6;
hence mi A c= A by TARSKI:def 3; :: thesis: verum