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:62;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;

now :: thesis: for x being object st x in Seg (len p) holds
(([#] (p,d)) | (Seg (len p))) . x = p . x

let x be object ; :: 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:47;
hence (([#] (p,d)) | (Seg (len p))) . x = p . x by A2, A3, Th20; :: thesis: verum

end;

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