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:90;
then reconsider f = {} as Function of [:A,A:],REAL by RELSET_1:12;
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 ) )
thus f . (x,x) = 0 ; :: thesis: ( x <> y implies f . (x,y) = 1 )
x = {} by A1, SUBSET_1:def 1
.= y by A1, SUBSET_1:def 1 ;
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 in REAL & 1 in REAL ) by XREAL_0:def 1;
then ( {0,1} c= REAL & rng (chi (([:A,A:] \ (id A)),[:A,A:])) c= {0,1} ) by ZFMISC_1:32;
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:4;
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:37; :: 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;