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

proof

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

proof

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

end;

thus ( ex y being object st [y,x] in Total X implies x in X ) by ZFMISC_1:87; :: thesis: verum

end;

hence rng (Total X) = X by XTUPLE_0:def 13; :: thesis: verum