let B, A be set ; :: thesis: for R being Relation of A,B holds
( proj1 R = (R ~ ) .: B & proj2 R = R .: A )
let R be Relation of A,B; :: thesis: ( proj1 R = (R ~ ) .: B & proj2 R = R .: A )
thus proj1 R = dom R
.= rng (R ~ ) by RELAT_1:37
.= (R ~ ) .: B by RELSET_1:38 ; :: thesis: proj2 R = R .: A
thus proj2 R = rng R
.= R .: A by RELSET_1:38 ; :: thesis: verum