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

let b be Element of A; :: thesis: |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b
reconsider pa = p ^ <*a*> as FinSequence of A ;
len p < (len p) + 1 by NAT_1:13;
then ( not (len p) + 1 in dom p & dom p is finite & dom ({b} | p) c= dom p ) by FINSEQ_3:27, FUNCT_1:89;
then ( not (len p) + 1 in dom ({b} | p) & dom ({b} | p) is finite ) ;
then ( |.(p ^ <*a*>).| . b = card (dom ({b} | pa)) & |.p.| . b = card (dom ({b} | p)) & dom ({a} | (p ^ <*a*>)) = (dom ({a} | p)) \/ {((len p) + 1)} & (chi a) . a = 1 & ( a <> b implies ( dom ({b} | (p ^ <*a*>)) = dom ({b} | p) & (chi a) . b = 0 ) ) & card ((dom ({b} | p)) \/ {((len p) + 1)}) = (card (dom ({b} | p))) + 1 & ( b = a or b <> a ) & (|.p.| [*] (chi a)) . b = (|.p.| . b) + ((chi a) . b) ) by Def7, Th30, Th32, Th35, Th36, CARD_2:54;
hence |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b ; :: thesis: verum

end;

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