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