let V, C be set ; :: thesis: for B being Element of Fin (PFuncs V,C)
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let B be Element of Fin (PFuncs V,C); :: thesis: for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
let a be finite set ; :: thesis: ( a in B & ( for b being finite set st b in B & b c= a holds
b = a ) implies a in mi B )
assume A1: ( a in B & ( for s being finite set st s in B & s c= a holds
s = a ) ) ; :: thesis: a in mi B
A2: for s being Element of PFuncs V,C holds
( ( s in B & s c= a ) iff s = a ) by A1;
B c= PFuncs V,C by FINSUB_1:def 5;
then reconsider a' = a as Element of PFuncs V,C by A1;
a' in { t where t is Element of PFuncs V,C : ( t is finite & ( for s being Element of PFuncs V,C holds
( ( s in B & s c= t ) iff s = t ) ) ) } by A2;
hence a in mi B ; :: thesis: verum