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 that
A1: a in B and
A2: for s being finite set st s in B & s c= a holds
s = a ; :: thesis: a in mi B
B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
for s being Element of PFuncs (V,C) holds
( ( s in B & s c= a ) iff s = a ) by A1, A2;
then a9 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 ) ) ) } ;
hence a in mi B ; :: thesis: verum