let X be set ; :: thesis: for P1, P2, R being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds
P1 = P2
let P1, P2, R 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 Th30, Th45;
hence ( rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X implies P1 = P2 ) by Th47; :: thesis: verum