let X be set ; :: thesis: for p being FinSequence holds
( p | X is FinSubsequence & X | p is FinSubsequence )
let p be FinSequence; :: thesis: ( p | X is FinSubsequence & X | p is FinSubsequence )
A1: dom p = Seg (len p) by Def3;
A2: dom (p | X) c= dom p by RELAT_1:89;
dom (X | p) c= dom p by FUNCT_1:89;
hence ( p | X is FinSubsequence & X | p is FinSubsequence ) by A1, A2, Def12; :: thesis: verum