let n be Element of NAT ; :: thesis: for p', q' being XFinSequence st n <= dom p' holds
(p' ^ q') | n = p' | n
let p', q' be XFinSequence; :: thesis: ( n <= dom p' implies (p' ^ q') | n = p' | n )
assume n <= dom p' ; :: thesis: (p' ^ q') | n = p' | n
then n c= dom p' by NAT_1:40;
then ((p' ^ q') | (dom p')) | n = (p' ^ q') | n by RELAT_1:103;
hence (p' ^ q') | n = p' | n by Th1; :: thesis: verum