let D be non empty set ; :: thesis: for d being Element of D
for p, q being FinSequence of D holds ([#] ((p ^ q),d)) | (dom p) = p
let d be Element of D; :: thesis: for p, q being FinSequence of D holds ([#] ((p ^ q),d)) | (dom p) = p
let p, q be FinSequence of D; :: thesis: ([#] ((p ^ q),d)) | (dom p) = p
set k = len p;
set f = [#] ((p ^ q),d);
Seg (len p) c= NAT ;
then Seg (len p) c= dom ([#] ((p ^ q),d)) by FUNCT_2:def 1;
then A1: dom (([#] ((p ^ q),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 ^ q),d)) | (Seg (len p))) . x = p . x

let x be object ; :: thesis: ( x in Seg (len p) implies (([#] ((p ^ q),d)) | (Seg (len p))) . x = p . x )
len p <= (len p) + (len q) by NAT_1:12;
then len p <= len (p ^ q) by FINSEQ_1:22;
then A3: ( Seg (len (p ^ q)) = dom (p ^ q) & Seg (len p) c= Seg (len (p ^ q)) ) by FINSEQ_1:5, FINSEQ_1:def 3;
assume A4: x in Seg (len p) ; :: thesis: (([#] ((p ^ q),d)) | (Seg (len p))) . x = p . x
then (([#] ((p ^ q),d)) | (Seg (len p))) . x = ([#] ((p ^ q),d)) . x by A1, FUNCT_1:47;
hence (([#] ((p ^ q),d)) | (Seg (len p))) . x = (p ^ q) . x by A4, A3, Th20
.= p . x by A2, A4, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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