let n be 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