let v be set ; :: thesis:
assume A1: v in rng (p | Y) ; :: thesis:
consider x being set such that
A2: x in dom (p | Y) and
A3: v = (p | Y) . x by A1, FUNCT_1:def 5;
A4: x in Y by A2, PARTFUN1:def 4;
then A5: (p | Y) . x = p . x by FUNCT_1:72;
x in X by A4;
then x in dom p by PARTFUN1:def 4;
then p . x in rng p by FUNCT_1:12;
hence v is RelStr by A3, A5, YELLOW_1:def 3; :: thesis:

end;