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