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 object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in Y |` (P * R) iff [x,b] in P * (Y |` R) )
let y be object ; :: 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 A1: [x,y] in Y |` (P * R) ; :: thesis: [x,y] in P * (Y |` R)
then [x,y] in P * R by Def10;
then consider a being object such that
A2: [x,a] in P and
A3: [a,y] in R by Def6;
y in Y by A1, Def10;
then [a,y] in Y |` R by A3, Def10;
hence [x,y] in P * (Y |` R) by A2, Def6; :: thesis: verum
end;
assume [x,y] in P * (Y |` R) ; :: thesis: [x,y] in Y |` (P * R)
then consider a being object such that
A4: [x,a] in P and
A5: [a,y] in Y |` R by Def6;
[a,y] in R by A5, Def10;
then A6: [x,y] in P * R by A4, Def6;
y in Y by A5, Def10;
hence [x,y] in Y |` (P * R) by A6, Def10; :: thesis: verum