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