let A be non empty set ; :: thesis: for a being Element of A holds |.<*a*>.| = chi a
let a be Element of A; :: thesis: |.<*a*>.| = chi a
A1: rng <*a*> = {a} by FINSEQ_1:56;

now

let b be Element of A; :: thesis: |.<*a*>.| . b = (chi a) . b
set x = b;
A2: <*a*> = (rng <*a*>) | <*a*> by RELAT_1:125;
( a <> b implies {b} misses {a} ) by ZFMISC_1:17;
then ( {b} | <*a*> = ({b} /\ (rng <*a*>)) | <*a*> & ( a <> b implies {b} /\ {a} = {} ) ) by A2, RELAT_1:127, XBOOLE_0:def 7;
then ( dom <*a*> = Seg 1 & card (Seg 1) = 1 & (chi a) . a = 1 & {a} | <*a*> = <*a*> & ( b <> a implies ( {b} | <*a*> = {} & (chi a) . b = 0 ) ) ) by A1, Th32, FINSEQ_1:55, FINSEQ_1:78, RELAT_1:125;
hence |.<*a*>.| . b = (chi a) . b by Def7, CARD_1:47, RELAT_1:60; :: thesis: verum

end;

hence |.<*a*>.| = chi a by Th33; :: thesis: verum