let B be non empty functional set ; :: thesis: for f being Function st f = union B holds
( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )
let f be Function; :: thesis: ( f = union B implies ( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } ) )
assume A1: f = union B ; :: thesis: ( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )
set X = { (dom g) where g is Element of B : verum } ;

now :: thesis: for x being object holds
( ( x in dom f implies ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } ) ) & ( ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } ) implies x in dom f ) )

let x be object ; :: thesis: ( ( x in dom f implies ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } ) ) & ( ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } ) implies x in dom f ) )

hereby :: thesis: ( ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } ) implies x in dom f )

assume x in dom f ; :: thesis: ex Z being set st
( x in Z & Z in { (dom g) where g is Element of B : verum } )
then [x,(f . x)] in f by Th1;
then consider g being set such that
A2: [x,(f . x)] in g and
A3: g in B by A1, TARSKI:def 4;
reconsider g = g as Function by A3;
take Z = dom g; :: thesis: ( x in Z & Z in { (dom g) where g is Element of B : verum } )
thus ( x in Z & Z in { (dom g) where g is Element of B : verum } ) by A2, A3, Th1; :: thesis: verum

end;

given Z being set such that A4: x in Z and
A5: Z in { (dom g) where g is Element of B : verum } ; :: thesis: x in dom f
consider g being Element of B such that
A6: Z = dom g by A5;
[x,(g . x)] in g by A4, A6, Th1;
then [x,(g . x)] in f by A1, TARSKI:def 4;
hence x in dom f by Th1; :: thesis: verum

end;

hence dom f = union { (dom g) where g is Element of B : verum } by TARSKI:def 4; :: thesis: rng f = union { (rng g) where g is Element of B : verum }
set X = { (rng g) where g is Element of B : verum } ;

now :: thesis: for y being object holds
( ( y in rng f implies ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } ) ) & ( ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } ) implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } ) ) & ( ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } ) implies y in rng f ) )

hereby :: thesis: ( ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } ) implies y in rng f )

assume y in rng f ; :: thesis: ex Z being set st
( y in Z & Z in { (rng g) where g is Element of B : verum } )
then consider x being object such that
A7: ( x in dom f & y = f . x ) by Def3;
[x,y] in f by A7, Th1;
then consider g being set such that
A8: [x,y] in g and
A9: g in B by A1, TARSKI:def 4;
reconsider g = g as Function by A9;
take Z = rng g; :: thesis: ( y in Z & Z in { (rng g) where g is Element of B : verum } )
( x in dom g & y = g . x ) by A8, Th1;
hence ( y in Z & Z in { (rng g) where g is Element of B : verum } ) by A9, Def3; :: thesis: verum

end;

given Z being set such that A10: y in Z and
A11: Z in { (rng g) where g is Element of B : verum } ; :: thesis: y in rng f
consider g being Element of B such that
A12: Z = rng g by A11;
consider x being object such that
A13: ( x in dom g & y = g . x ) by A10, A12, Def3;
[x,y] in g by A13, Th1;
then [x,y] in f by A1, TARSKI:def 4;
hence y in rng f by XTUPLE_0:def 13; :: thesis: verum

end;

hence rng f = union { (rng g) where g is Element of B : verum } by TARSKI:def 4; :: thesis: verum