defpred S₁[ 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}:] & S₁[x] ) ) from XBOOLE_0:sch 1();
F c= Funcs (X,{x1,x2})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in Funcs (X,{x1,x2}) )
assume x in F ; :: thesis: x in Funcs (X,{x1,x2})
then ex f being Function of X,{x1,x2} st
( x = f & card (f " {x1}) = k ) by A1;
hence x in Funcs (X,{x1,x2}) by FUNCT_2:8; :: thesis: verum

end;

then reconsider F = F as Subset of (Funcs (X,{x1,x2})) ;
take F ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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 ) ; :: thesis: x in F
thus x in F by A1, A2; :: thesis: verum