let A, B be set ; :: thesis: for R being Relation of A,B holds (id A) * R = R * (id B)
let R be Relation of A,B; :: thesis: (id A) * R = R * (id B)
(id A) * R = R by FUNCT_2:17
.= R * (id B) by FUNCT_2:17 ;
hence (id A) * R = R * (id B) ; :: thesis: verum