let V, C be set ; :: thesis: for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
let B be Element of Fin (PFuncs (V,C)); :: thesis: for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
defpred S₁[ set , set ] means $1 c= $2;
let b be finite set ; :: thesis: ( b in B implies ex c being set st
( c c= b & c in mi B ) )
assume A1: b in B ; :: thesis: ex c being set st
( c c= b & c in mi B )
A2: B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V,C) by A1;
A3: for a, b, c being Element of PFuncs (V,C) st S₁[a,b] & S₁[b,c] holds
S₁[a,c] by XBOOLE_1:1;
A4: for a being Element of PFuncs (V,C) holds S₁[a,a] ;
for a being Element of PFuncs (V,C) st a in B holds
ex b being Element of PFuncs (V,C) st
( b in B & S₁[b,a] & ( for c being Element of PFuncs (V,C) st c in B & S₁[c,b] holds
S₁[b,c] ) ) from FRAENKEL:sch 23(A4, A3);
then consider c being Element of PFuncs (V,C) such that
A5: c in B and
A6: c c= b9 and
A7: for a being Element of PFuncs (V,C) st a in B & a c= c holds
c c= a by A1;
take c ; :: thesis: ( c c= b & c in mi B )
thus c c= b by A6; :: thesis: c in mi B
for b being finite set st b in B & b c= c holds
b = c by A2, A7;
hence c in mi B by A5, A6, Th7; :: thesis: verum