let A be non empty set ; :: thesis: for a, b being Element of A holds

( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

let a, b be Element of A; :: thesis: ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

A1: ( b <> a implies not b in {a} ) by TARSKI:def 1;

a in {a} by TARSKI:def 1;

hence ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) by A1, FUNCT_3:def 3; :: thesis: verum

( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

let a, b be Element of A; :: thesis: ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

A1: ( b <> a implies not b in {a} ) by TARSKI:def 1;

a in {a} by TARSKI:def 1;

hence ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) by A1, FUNCT_3:def 3; :: thesis: verum