let A be non empty set ; :: thesis: for a being Element of A
for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)
let a be Element of A; :: thesis: for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)
let p be FinSequence of A; :: thesis: |.(p ^ <*a*>).| = |.p.| [*] (chi a)

now :: thesis: for b being Element of A holds |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b

reconsider pa = p ^ <*a*> as FinSequence of A ;
let b be Element of A; :: thesis: |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b
( len p < (len p) + 1 & dom ({b} |` p) c= dom p ) by FUNCT_1:56, NAT_1:13;
then A1: not (len p) + 1 in dom ({b} |` p) by FINSEQ_3:25;
A2: ( |.(p ^ <*a*>).| . b = card (dom ({b} |` pa)) & |.p.| . b = card (dom ({b} |` p)) ) by Def7;
A3: ( a <> b implies ( dom ({b} |` (p ^ <*a*>)) = dom ({b} |` p) & (chi a) . b = 0 ) ) by Th31, Th35;
A4: (|.p.| [*] (chi a)) . b = (|.p.| . b) + ((chi a) . b) by Th29;
( dom ({a} |` (p ^ <*a*>)) = (dom ({a} |` p)) \/ {((len p) + 1)} & (chi a) . a = 1 ) by Th31, Th34;
hence |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b by A1, A2, A3, A4, CARD_2:41; :: thesis: verum

end;

hence |.(p ^ <*a*>).| = |.p.| [*] (chi a) by Th32; :: thesis: verum