let A, B 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:20
.= (R ~) .: B by RELSET_1:22 ; :: thesis: proj2 R = R .: A
thus proj2 R = rng R
.= R .: A by RELSET_1:22 ; :: thesis: verum