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

hereby :: thesis: ( [a,b] in (R ~) * (P ~) implies [a,b] in (P * R) ~ )

assume [a,b] in (P * R) ~ ; :: thesis: [a,b] in (R ~) * (P ~)
then [b,a] in P * R by Def7;
then consider y being set such that
A1: ( [b,y] in P & [y,a] in R ) by Def8;
( [y,b] in P ~ & [a,y] in R ~ ) by A1, Def7;
hence [a,b] in (R ~) * (P ~) by Def8; :: thesis: verum

end;

assume [a,b] in (R ~) * (P ~) ; :: thesis: [a,b] in (P * R) ~
then consider y being set such that
A2: ( [a,y] in R ~ & [y,b] in P ~ ) by Def8;
( [y,a] in R & [b,y] in P ) by A2, Def7;
then [b,a] in P * R by Def8;
hence [a,b] in (P * R) ~ by Def7; :: thesis: verum