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 ) )

A3: {0 ,1} c= REAL by ZFMISC_1:38;
rng (chi ([:A,A:] \ (id A)),[:A,A:]) c= {0 ,1} by FUNCT_3:48;
then A4: rng (chi ([:A,A:] \ (id A)),[:A,A:]) c= REAL by A3, 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 A4, 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 ) )
A5: [x,y] in [:A,A:] by A2, ZFMISC_1:def 2;
[:A,A:] \ ([:A,A:] \ (id A)) = [:A,A:] /\ (id A) by XBOOLE_1:48
.= id A by RELSET_1:28, 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 not [x,y] in id A by RELAT_1:def 10;
then [x,y] in [:A,A:] \ (id A) by A5, XBOOLE_0:def 5;
hence char . x,y = 1 by FUNCT_3:def 3; :: thesis: verum

end;

end;