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