let X be set ; :: thesis: rng (Total X) = X
for x being set holds
( x in X iff ex y being set st [y,x] in Total X )

proof

let x be set ; :: thesis: ( x in X iff ex y being set st [y,x] in Total X )
thus ( x in X implies ex y being set st [y,x] in Total X ) :: thesis: ( ex y being set st [y,x] in Total X implies x in X )

proof

assume A1: x in X ; :: thesis: ex y being set st [y,x] in Total X
take x ; :: thesis: [x,x] in Total X
[x,x] in [:X,X:] by A1, ZFMISC_1:106;
hence [x,x] in Total X by EQREL_1:def 1; :: thesis: verum

end;

given y being set such that A2: [y,x] in Total X ; :: thesis: x in X
thus x in X by A2, ZFMISC_1:106; :: thesis: verum

end;

hence rng (Total X) = X by RELAT_1:def 5; :: thesis: verum