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 :: thesis: for b being Element of A holds |.<*a*>.| . b = (chi a) . b
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} = {} ) ;
A4: ( (chi a) . a = 1 & {a} |` <*a*> = <*a*> ) by A1, Th31;
<*a*> = (rng <*a*>) |` <*a*> ;
then {b} |` <*a*> = ({b} /\ (rng <*a*>)) |` <*a*> by RELAT_1:96;
then ( b <> a implies ( {b} |` <*a*> = {} & (chi a) . b = 0 ) ) by A1, A3, Th31;
hence |.<*a*>.| . b = (chi a) . b by A2, A4, Def7, CARD_1:27, RELAT_1:38; :: thesis: verum
end;
hence |.<*a*>.| = chi a by Th32; :: thesis: verum