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: ( dom <*a*> = Seg 1 & card (Seg 1) = 1 ) by FINSEQ_1:55, FINSEQ_1:78;
( a <> b implies {b} misses {a} ) by ZFMISC_1:17;
then A3: ( a <> b implies {b} /\ {a} = {} ) by XBOOLE_0:def 7;
A4: ( (chi a) . a = 1 & {a} | <*a*> = <*a*> ) by A1, Th32, RELAT_1:125;
<*a*> = (rng <*a*>) | <*a*> by RELAT_1:125;
then {b} | <*a*> = ({b} /\ (rng <*a*>)) | <*a*> by RELAT_1:127;
then ( b <> a implies ( {b} | <*a*> = {} & (chi a) . b = 0 ) ) by A1, A3, Th32;
hence |.<*a*>.| . b = (chi a) . b by A2, A4, Def7, CARD_1:47, RELAT_1:60; :: thesis: verum

end;

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