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) & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:91;

now

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

end;

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