let p, q be FinSequence; :: thesis: p = (p ^ q) | (dom p)
A1: ( dom (p ^ q) = Seg ((len p) + (len q)) & len p <= (len p) + (len q) & dom p = Seg (len p) ) by Def3, Def7, NAT_1:12;
then A2: dom p = (dom (p ^ q)) /\ (Seg (len p)) by Th9;
for x being set st x in dom p holds
p . x = (p ^ q) . x by Def7;
hence p = (p ^ q) | (dom p) by A1, A2, FUNCT_1:68; :: thesis: verum