let V, C be set ; :: thesis: for B being Element of Fin (PFuncs V,C)
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
let B be Element of Fin (PFuncs V,C); :: thesis: for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
let b be finite set ; :: thesis: ( b in B implies ex c being set st
( c c= b & c in mi B ) )
A1: B c= PFuncs V,C by FINSUB_1:def 5;
assume A2: b in B ; :: thesis: ex c being set st
( c c= b & c in mi B )
then reconsider b' = b as Element of PFuncs V,C by A1;
defpred S₁[ set , set ] means $1 c= $2;
A3: for a being Element of PFuncs V,C holds S₁[a,a] ;
A4: for a, b, c being Element of PFuncs V,C st S₁[a,b] & S₁[b,c] holds
S₁[a,c] by XBOOLE_1:1;
for a being Element of PFuncs V,C st a in B holds
ex b being Element of PFuncs V,C st
( b in B & S₁[b,a] & ( for c being Element of PFuncs V,C st c in B & S₁[c,b] holds
S₁[b,c] ) ) from FRAENKEL:sch 23(A3, A4);
then consider c being Element of PFuncs V,C such that
A5: c in B and
A6: c c= b' and
A7: for a being Element of PFuncs V,C st a in B & a c= c holds
c c= a by A2;
take c ; :: thesis: ( c c= b & c in mi B )
A8: c is finite by A6;
thus c c= b by A6; :: thesis: c in mi B

now

let b be finite set ; :: thesis: ( b in B & b c= c implies b = c )
assume that
A9: b in B and
A10: b c= c ; :: thesis: b = c
reconsider b' = b as Element of PFuncs V,C by A1, A9;
c c= b' by A7, A9, A10;
hence b = c by A10, XBOOLE_0:def 10; :: thesis: verum

end;

hence c in mi B by A5, A8, Th7; :: thesis: verum