let p be FinSequence; :: thesis: for n, m being Nat st m <= n holds
(p | n) | m = p | m
let n, m be Nat; :: thesis: ( m <= n implies (p | n) | m = p | m )
assume m <= n ; :: thesis: (p | n) | m = p | m
then Seg m c= Seg n by Th7;
hence (p | n) | m = p | m by RELAT_1:103; :: thesis: verum