let P, R be Relation; :: thesis: (P * R) ~ = (R ~) * (P ~)
let a be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [a,b] in (P * R) ~ iff [a,b] in (R ~) * (P ~) )
let b be object ; :: 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 Def5;
then consider y being object such that
A1: ( [b,y] in P & [y,a] in R ) by Def6;
( [y,b] in P ~ & [a,y] in R ~ ) by A1, Def5;
hence [a,b] in (R ~) * (P ~) by Def6; :: thesis: verum

end;

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