let X, Y be non empty set ; :: thesis: for A being set
for F being sequence of X
for G being sequence of Y st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let A be set ; :: thesis: for F being sequence of X
for G being sequence of Y st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let F be sequence of X; :: thesis: for G being sequence of Y st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let G be sequence of Y; :: thesis: ( ( for n being Element of NAT holds G . n = A /\ (F . n) ) implies union (rng G) = A /\ (union (rng F)) )
assume A1: for n being Element of NAT holds G . n = A /\ (F . n) ; :: thesis: union (rng G) = A /\ (union (rng F))

now :: thesis: for r being object st r in union (rng G) holds
r in A /\ (union (rng F))

let r be object ; :: thesis: ( r in union (rng G) implies r in A /\ (union (rng F)) )
assume r in union (rng G) ; :: thesis: r in A /\ (union (rng F))
then consider E being set such that
A2: r in E and
A3: E in rng G by TARSKI:def 4;
consider s being object such that
A4: s in dom G and
A5: E = G . s by A3, FUNCT_1:def 3;
reconsider s = s as Element of NAT by A4;
A6: r in A /\ (F . s) by A1, A2, A5;
then A7: r in A by XBOOLE_0:def 4;
A8: F . s in rng F by FUNCT_2:4;
r in F . s by A6, XBOOLE_0:def 4;
then r in union (rng F) by A8, TARSKI:def 4;
hence r in A /\ (union (rng F)) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

then A9: union (rng G) c= A /\ (union (rng F)) ;

now :: thesis: for r being object st r in A /\ (union (rng F)) holds
r in union (rng G)

let r be object ; :: thesis: ( r in A /\ (union (rng F)) implies r in union (rng G) )
assume A10: r in A /\ (union (rng F)) ; :: thesis: r in union (rng G)
then A11: r in A by XBOOLE_0:def 4;
r in union (rng F) by A10, XBOOLE_0:def 4;
then consider E being set such that
A12: r in E and
A13: E in rng F by TARSKI:def 4;
consider s being object such that
A14: s in dom F and
A15: E = F . s by A13, FUNCT_1:def 3;
reconsider s = s as Element of NAT by A14;
A16: G . s in rng G by FUNCT_2:4;
A /\ E = G . s by A1, A15;
then r in G . s by A11, A12, XBOOLE_0:def 4;
hence r in union (rng G) by A16, TARSKI:def 4; :: thesis: verum

end;

then A /\ (union (rng F)) c= union (rng G) ;
hence union (rng G) = A /\ (union (rng F)) by A9, XBOOLE_0:def 10; :: thesis: verum