let X be set ; :: thesis: for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds
P1 = P2
let P2, R, P1 be Relation; :: thesis: ( rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X implies P1 = P2 )
( (P2 * R) * P1 = P2 * (R * P1) & (id (dom P1)) * P1 = P1 ) by Th55, Th77;
hence ( rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X implies P1 = P2 ) by Th79; :: thesis: verum