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 ) )
( chi a = chi {a},A & a in {a} & ( b <> a implies not b in {a} ) ) by TARSKI:def 1;
hence ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) by FUNCT_3:def 3; :: thesis: verum