let p, q be XFinSequence; :: thesis: (p ^ q) | (dom p) = p
set r = (p ^ q) | (dom p);

A1: now :: thesis: for k being Nat st k < len p holds
((p ^ q) | (dom p)) . k = p . k

let k be Nat; :: thesis: ( k < len p implies ((p ^ q) | (dom p)) . k = p . k )
assume A2: k < len p ; :: thesis: ((p ^ q) | (dom p)) . k = p . k
A3: k in dom p by A2, Lm1;
then A4: (p ^ q) . k = p . k by Def3;
k + 0 < (len p) + (len q) by A2, XREAL_1:8;
then k in Segm ((len p) + (len q)) by NAT_1:44;
then k in dom (p ^ q) by Def3;
then k in (dom (p ^ q)) /\ (dom p) by A3, XBOOLE_0:def 4;
hence ((p ^ q) | (dom p)) . k = p . k by A4, FUNCT_1:48; :: thesis: verum

end;

dom p c= dom (p ^ q) by Th19;
then len ((p ^ q) | (dom p)) = len p by RELAT_1:62;
hence (p ^ q) | (dom p) = p by A1, Th8; :: thesis: verum