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