let B be functional non empty 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

let x be set ; :: 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 FUNCT_1:8;
then consider g being set such that
A2: ( [x,(f . x)] in g & g in B ) by A1, TARSKI:def 4;
reconsider g = g as Function by A2;
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, FUNCT_1:8; :: thesis: verum

end;

given Z being set such that A3: ( x in Z & Z in { (dom g) where g is Element of B : verum } ) ; :: thesis: x in dom f
consider g being Element of B such that
A4: Z = dom g by A3;
[x,(g . x)] in g by A3, A4, FUNCT_1:8;
then [x,(g . x)] in f by A1, TARSKI:def 4;
hence x in dom f by FUNCT_1:8; :: 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

let y be set ; :: 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 set such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
[x,y] in f by A5, FUNCT_1:8;
then consider g being set such that
A6: ( [x,y] in g & g in B ) by A1, TARSKI:def 4;
reconsider g = g as Function by A6;
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 A6, FUNCT_1:8;
hence ( y in Z & Z in { (rng g) where g is Element of B : verum } ) by A6, FUNCT_1:def 5; :: thesis: verum

end;

given Z being set such that A7: ( y in Z & Z in { (rng g) where g is Element of B : verum } ) ; :: thesis: y in rng f
consider g being Element of B such that
A8: Z = rng g by A7;
consider x being set such that
A9: ( x in dom g & y = g . x ) by A7, A8, FUNCT_1:def 5;
[x,y] in g by A9, FUNCT_1:8;
then [x,y] in f by A1, TARSKI:def 4;
hence y in rng f by RELAT_1:20; :: thesis: verum

end;

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