let I1, I2 be Subset of (union (rng F)); :: thesis: ( ( for z being set holds
( z in I1 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) ) & ( for z being set holds
( z in I2 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) ) implies I1 = I2 )
assume that
A2: for z being set holds
( z in I1 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) and
A3: for z being set holds
( z in I2 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) ; :: thesis: I1 = I2
for z being object holds
( z in I1 iff z in I2 )

proof

let z be object ; :: thesis: ( z in I1 iff z in I2 )
( z in I1 iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) by A2;
hence ( z in I1 iff z in I2 ) by A3; :: thesis: verum

end;

hence I1 = I2 by TARSKI:2; :: thesis: verum