per cases ( A is empty or not A is empty ) ;

suppose A1: A is empty ; :: thesis: ex b₁ being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b₁ . x,x = 0 & ( x <> y implies b₁ . x,y = 1 ) )

then [:A,A:] = {} by ZFMISC_1:113;
then reconsider f = {} as Function of [:A,A:],REAL by RELSET_1:25;
take f ; :: thesis: for x, y being Element of A holds
( f . x,x = 0 & ( x <> y implies f . x,y = 1 ) )
let x, y be Element of A; :: thesis: ( f . x,x = 0 & ( x <> y implies f . x,y = 1 ) )
dom {} = {} ;
hence f . x,x = 0 by FUNCT_1:def 4; :: thesis: ( x <> y implies f . x,y = 1 )
x = {} by A1, SUBSET_1:def 2
.= y by A1, SUBSET_1:def 2 ;
hence ( x <> y implies f . x,y = 1 ) ; :: thesis: verum

end;

suppose A2: not A is empty ; :: thesis: ex b₁ being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b₁ . x,x = 0 & ( x <> y implies b₁ . x,y = 1 ) )

( {0 ,1} c= REAL & rng (chi ([:A,A:] \ (id A)),[:A,A:]) c= {0 ,1} ) by FUNCT_3:48, ZFMISC_1:38;
then A3: rng (chi ([:A,A:] \ (id A)),[:A,A:]) c= REAL by XBOOLE_1:1;
dom (chi ([:A,A:] \ (id A)),[:A,A:]) = [:A,A:] by FUNCT_3:def 3;
then reconsider char = chi ([:A,A:] \ (id A)),[:A,A:] as Function of [:A,A:],REAL by A3, RELSET_1:11;
take char ; :: thesis: for x, y being Element of A holds
( char . x,x = 0 & ( x <> y implies char . x,y = 1 ) )
let x, y be Element of A; :: thesis: ( char . x,x = 0 & ( x <> y implies char . x,y = 1 ) )
[:A,A:] \ ([:A,A:] \ (id A)) = [:A,A:] /\ (id A) by XBOOLE_1:48
.= id A by XBOOLE_1:28 ;
then [x,x] in [:A,A:] \ ([:A,A:] \ (id A)) by A2, RELAT_1:def 10;
hence char . x,x = 0 by FUNCT_3:43; :: thesis: ( x <> y implies char . x,y = 1 )
assume x <> y ; :: thesis: char . x,y = 1
then A4: not [x,y] in id A by RELAT_1:def 10;
[x,y] in [:A,A:] by A2, ZFMISC_1:def 2;
then [x,y] in [:A,A:] \ (id A) by A4, XBOOLE_0:def 5;
hence char . x,y = 1 by FUNCT_3:def 3; :: thesis: verum

end;

end;