now :: thesis: for v being set st v in rng (p | Y) holds
v is RelStr
let v be set ; :: thesis: ( v in rng (p | Y) implies v is RelStr )
assume v in rng (p | Y) ; :: thesis: v is RelStr
then consider x being object such that
A1: x in dom (p | Y) and
A2: v = (p | Y) . x by FUNCT_1:def 3;
A3: x in Y by A1;
then A4: (p | Y) . x = p . x by FUNCT_1:49;
x in X by A3;
then x in dom p by PARTFUN1:def 2;
then p . x in rng p by FUNCT_1:3;
hence v is RelStr by A2, A4, YELLOW_1:def 3; :: thesis: verum
end;
hence p | Y is RelStr-yielding by YELLOW_1:def 3; :: thesis: verum