let D be non empty set ; :: thesis: for d being Element of D
for p being FinSequence of D holds ([#] p,d) | (dom p) = p
let d be Element of D; :: thesis: for p being FinSequence of D holds ([#] p,d) | (dom p) = p
let p be FinSequence of D; :: thesis: ([#] p,d) | (dom p) = p
set k = len p;
set f = [#] p,d;
Seg (len p) c= NAT ;
then Seg (len p) c= dom ([#] p,d) by FUNCT_2:def 1;
then A1: dom (([#] p,d) | (Seg (len p))) = Seg (len p) by RELAT_1:91;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;

now

let x be set ; :: thesis: ( x in Seg (len p) implies (([#] p,d) | (Seg (len p))) . x = p . x )
assume A3: x in Seg (len p) ; :: thesis: (([#] p,d) | (Seg (len p))) . x = p . x
then (([#] p,d) | (Seg (len p))) . x = ([#] p,d) . x by A1, FUNCT_1:70;
hence (([#] p,d) | (Seg (len p))) . x = p . x by A2, A3, Th22; :: thesis: verum

end;

hence ([#] p,d) | (dom p) = p by A1, A2, FUNCT_1:9; :: thesis: verum