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 & X in rng g ) by TARSKI:def 4;
consider u2 being set such that
A2: ( u2 in dom g & X = g . u2 ) by A1, FUNCT_1:def 5;
take u2 ; :: thesis: ( u2 in dom g & u1 in g . u2 )
thus ( u2 in dom g & u1 in g . u2 ) by A1, A2; :: thesis: verum