let Y be set ; :: thesis: for P, R being Relation holds Y | (P * R) = P * (Y | R)
let P, R be Relation; :: thesis: Y | (P * R) = P * (Y | R)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in Y | (P * R) iff [x,b] in P * (Y | R) )
let y be set ; :: thesis: ( [x,y] in Y | (P * R) iff [x,y] in P * (Y | R) )

hereby :: thesis: ( [x,y] in P * (Y | R) implies [x,y] in Y | (P * R) )

assume A5: [x,y] in Y | (P * R) ; :: thesis: [x,y] in P * (Y | R)
then [x,y] in P * R by Def12;
then consider a being set such that
A6: [x,a] in P and
A7: [a,y] in R by Def8;
y in Y by A5, Def12;
then [a,y] in Y | R by A7, Def12;
hence [x,y] in P * (Y | R) by A6, Def8; :: thesis: verum

end;

assume [x,y] in P * (Y | R) ; :: thesis: [x,y] in Y | (P * R)
then consider a being set such that
A2: [x,a] in P and
A3: [a,y] in Y | R by Def8;
[a,y] in R by A3, Def12;
then A4: [x,y] in P * R by A2, Def8;
y in Y by A3, Def12;
hence [x,y] in Y | (P * R) by A4, Def12; :: thesis: verum