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 Segm n c= Segm (len p) by NAT_1:39;
then ((p ^ q) | (dom p)) | n = (p ^ q) | n by RELAT_1:74;
hence (p ^ q) | n = p | n by Th54; :: thesis: verum