let A, B be set ; :: thesis: for U1, U2 being non empty set
for Q being quasi_total Relation of B,U1
for R being quasi_total Relation of B,U2
for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds
((P * Q) * (Q ~)) * R = P * R
let U1, U2 be non empty set ; :: thesis: for Q being quasi_total Relation of B,U1
for R being quasi_total Relation of B,U2
for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds
((P * Q) * (Q ~)) * R = P * R
let Q be quasi_total Relation of B,U1; :: thesis: for R being quasi_total Relation of B,U2
for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds
((P * Q) * (Q ~)) * R = P * R
let R be quasi_total Relation of B,U2; :: thesis: for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds
((P * Q) * (Q ~)) * R = P * R
let P be Relation of A,B; :: thesis: ( ((P * Q) * (Q ~)) * R is Function-like implies ((P * Q) * (Q ~)) * R = P * R )
reconsider QQ = Q as B -defined total Relation ;
reconsider RR = R as B -defined total Relation ;
A1: ( dom R = B & rng P c= B ) by PARTFUN1:def 2;
assume ((P * Q) * (Q ~)) * R is Function-like ; :: thesis: ((P * Q) * (Q ~)) * R = P * R
hence ((P * Q) * (Q ~)) * R = P * R by A1, Lm43; :: thesis: verum