defpred S1[ object ] means ex f being Function of X,{x1,x2} st
( $1 = f & card (f " {x1}) = k );
consider F being set such that
A1:
for x being object holds
( x in F iff ( x in bool [:X,{x1,x2}:] & S1[x] ) )
from XBOOLE_0:sch 1();
F c= Funcs (X,{x1,x2})
then reconsider F = F as Subset of (Funcs (X,{x1,x2})) ;
take
F
; for x being set holds
( x in F iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) )
let x be set ; ( x in F iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) )
thus
( x in F implies ex f being Function of X,{x1,x2} st
( x = f & card (f " {x1}) = k ) )
by A1; ( ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) implies x in F )
given f being Function of X,{x1,x2} such that A2:
( x = f & card (f " {x1}) = k )
; x in F
thus
x in F
by A1, A2; verum