let Y be set ; :: thesis: for R, P being Relation
for Q being Y -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds
((P * Q) * (Q ~)) * R = P * R
let R, P be Relation; :: thesis: for Q being Y -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds
((P * Q) * (Q ~)) * R = P * R
let Q be Y -defined Relation; :: thesis: ( Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R implies ((P * Q) * (Q ~)) * R = P * R )
assume Q is total ; :: thesis: ( not R is Y -defined or not ((P * Q) * (Q ~)) * R is Function-like or not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R )
then reconsider QQ = Q as Y -defined total Relation ;
set tQ = QQ ~ ;
assume R is Y -defined ; :: thesis: ( not ((P * Q) * (Q ~)) * R is Function-like or not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R )
then reconsider RR = R as Y -defined Relation ;
assume ((P * Q) * (Q ~)) * R is Function-like ; :: thesis: ( not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R )
then reconsider f = ((P * Q) * (QQ ~)) * R as Function ;
B0: f = (P * Q) * ((QQ ~) * R) by RELAT_1:36
.= P * (Q * ((QQ ~) * R)) by RELAT_1:36
.= P * ((Q * (QQ ~)) * RR) by RELAT_1:36 ;
(id Y) * RR c= (Q * (QQ ~)) * RR by Th21, RELAT_1:30;
then Z1: RR | Y c= (Q * (QQ ~)) * RR by RELAT_1:65;
assume rng P c= dom R ; :: thesis: ((P * Q) * (Q ~)) * R = P * R
then B1: dom (P * R) = dom P by RELAT_1:27;
( dom (P * (Q * (QQ ~))) c= dom P & dom (((P * Q) * (QQ ~)) * R) c= dom ((P * Q) * (QQ ~)) ) by RELAT_1:25;
then ( dom ((P * Q) * (QQ ~)) c= dom P & dom f c= dom ((P * Q) * (QQ ~)) ) by RELAT_1:36;
then dom f c= dom (P * R) by B1, XBOOLE_1:1;
hence ((P * Q) * (Q ~)) * R = P * R by Z1, B0, Lm47, RELAT_1:29; :: thesis: verum