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