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)

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

hence
|.(p ^ <*a*>).| = |.p.| [*] (chi a)
by Th32; :: thesis: verumreconsider 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;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