let D be set ; :: thesis: for n being Nat
for pd being XFinSequence of D ex qd being XFinSequence of D st pd = (pd | n) ^ qd
let n be 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
consider q9 being XFinSequence such that
A1: pd = (pd | n) ^ q9 by AFINSQ_1:60;
rng q9 c= rng pd by A1, AFINSQ_1:25;
then rng q9 c= D by XBOOLE_1:1;
then q9 is XFinSequence of D by RELAT_1:def 19;
hence ex qd being XFinSequence of D st pd = (pd | n) ^ qd by A1; :: thesis: verum