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

end;

suppose A1:
A is empty
; :: thesis: ex b_{1} being Function of [:A,A:],REAL st

for x, y being Element of A holds

( b_{1} . (x,x) = 0 & ( x <> y implies b_{1} . (x,y) = 1 ) )

for x, y being Element of A holds

( b

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

suppose A2:
not A is empty
; :: thesis: ex b_{1} being Function of [:A,A:],REAL st

for x, y being Element of A holds

( b_{1} . (x,x) = 0 & ( x <> y implies b_{1} . (x,y) = 1 ) )

for x, y being Element of A holds

( b

( 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;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