let p', q' be XFinSequence; :: thesis: (p' ^ q') | (dom p') = p'
dom p' = len p' ;
then reconsider r = (p' ^ q') | (dom p') as XFinSequence by AFINSQ_1:12;

A1: now

let k be Element of NAT ; :: thesis: ( k < len p' implies r . k = p' . k )
assume A2: k < len p' ; :: thesis: r . k = p' . k
A3: k in dom p' by A2, NAT_1:45;
then A4: (p' ^ q') . k = p' . k by AFINSQ_1:def 4;
k + 0 < (len p') + (len q') by A2, XREAL_1:10;
then k in (len p') + (len q') by NAT_1:45;
then k in dom (p' ^ q') by AFINSQ_1:def 4;
then k in (dom (p' ^ q')) /\ (dom p') by A3, XBOOLE_0:def 4;
hence r . k = p' . k by A4, FUNCT_1:71; :: thesis: verum

end;

dom p' c= dom (p' ^ q') by AFINSQ_1:24;
then len r = len p' by RELAT_1:91;
hence (p' ^ q') | (dom p') = p' by A1, AFINSQ_1:11; :: thesis: verum