let U2, U1, U3 be non empty set ; :: thesis: for n being Nat
for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
let n be Nat; :: thesis: for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
let U be non empty Subset of U2; :: thesis: for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
let P be Relation of U1,U; :: 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)
set R = P * Q;
set LH = n -placesOf (P * Q);
set Pn = n -placesOf P;
set Qn = n -placesOf Q;
set RH = (n -placesOf P) * (n -placesOf Q);
( n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q) & (n -placesOf P) * (n -placesOf Q) c= n -placesOf (P * Q) ) by Lm12, Lm18;
hence n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q) by XBOOLE_0:def 10; :: thesis: verum