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:39;

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:38, FINSEQ_1:57;
( a <> b implies {b} misses {a} ) by ZFMISC_1:11;
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:94;
<*a*> = (rng <*a*>) | <*a*> by RELAT_1:94;
then {b} | <*a*> = ({b} /\ (rng <*a*>)) | <*a*> by RELAT_1:96;
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:27, RELAT_1:38; :: thesis: verum

end;

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