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;

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

hence
|.<*a*>.| = chi a
by Th32; :: thesis: verumlet 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;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