let g be Function; :: thesis: for u1 being set st u1 in Union g holds
ex u2 being set st
( u2 in dom g & u1 in g . u2 )
let u1 be set ; :: thesis: ( u1 in Union g implies ex u2 being set st
( u2 in dom g & u1 in g . u2 ) )
assume u1 in Union g ; :: thesis: ex u2 being set st
( u2 in dom g & u1 in g . u2 )
then u1 in union (rng g) by CARD_3:def 4;
then consider X being set such that
A1: u1 in X and
A2: X in rng g by TARSKI:def 4;
consider u2 being object such that
A3: ( u2 in dom g & X = g . u2 ) by A2, FUNCT_1:def 3;
take u2 ; :: thesis: ( u2 is set & u2 in dom g & u1 in g . u2 )
thus ( u2 is set & u2 in dom g & u1 in g . u2 ) by A1, A3; :: thesis: verum