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: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 ^ 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:35;
then A3: ( Seg (len (p ^ q)) = dom (p ^ q) & Seg (len p) c= Seg (len (p ^ q)) ) by FINSEQ_1:7, 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:70;
hence (([#] (p ^ q),d) | (Seg (len p))) . x = (p ^ q) . x by A4, A3, Th22
.= p . x by A2, A4, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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