let D be set ; :: thesis: for n being Element of NAT
for pd being XFinSequence of D ex qd being XFinSequence of D st pd = (pd | n) ^ qd
let n be Element of NAT ; :: thesis: for pd being XFinSequence of D ex qd being XFinSequence of D st pd = (pd | n) ^ qd
let pd be XFinSequence of D; :: thesis: ex qd being XFinSequence of D st pd = (pd | n) ^ qd
A1: rng pd c= D by RELAT_1:def 19;
consider q' being XFinSequence such that
A2: pd = (pd | n) ^ q' by Th4;
rng q' c= rng pd by A2, AFINSQ_1:28;
then rng q' c= D by A1, XBOOLE_1:1;
then q' is XFinSequence of D by RELAT_1:def 19;
hence ex qd being XFinSequence of D st pd = (pd | n) ^ qd by A2; :: thesis: verum