let Y be set ; :: thesis: for P, R 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 P, R 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 ;
A1: 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 RELAT_1:30, Th21;
then A2: RR | Y c= (Q * (QQ ~)) * RR by RELAT_1:65;
assume rng P c= dom R ; :: thesis: ((P * Q) * (Q ~)) * R = P * R
then A3: 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 A3;
hence ((P * Q) * (Q ~)) * R = P * R by A2, A1, RELAT_1:29, Lm42; :: thesis: verum