let U1, U2, U3 be non empty set ; :: thesis: for n being Nat
for P being Relation of U1,U2
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
let n be Nat; :: thesis: for P being Relation of U1,U2
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
reconsider U = U2 /\ U2 as non empty Subset of U2 ;
let P be Relation of U1,U2; :: thesis: for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
let Q be Relation of U2,U3; :: thesis: n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
reconsider PP = P as Relation of U1,U ;
n -placesOf (PP * Q) = (n -placesOf PP) * (n -placesOf Q) by Lm15;
hence n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q) ; :: thesis: verum