defpred S₁[ object , object ] means ( ( $1 in A implies $2 = 1 ) & ( not $1 in A implies $2 = 0 ) );
A1: for x being object st x in X holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in X implies ex y being object st S₁[x,y] )
assume x in X ; :: thesis: ex y being object st S₁[x,y]
( not x in A implies ex y being set st
( y = {} & ( x in A implies y = 1 ) & ( not x in A implies y = {} ) ) ) ;
hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

A2: for x, y1, y2 being object st x in X & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
ex f being Function st
( dom f = X & ( for x being object st x in X holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A2, A1);
hence ex b₁ being Function st
( dom b₁ = X & ( for x being object st x in X holds
( ( x in A implies b₁ . x = 1 ) & ( not x in A implies b₁ . x = 0 ) ) ) ) ; :: thesis: verum