let X be set ; :: thesis: for S being non empty Subset-Family of X
for F, G being Function of NAT ,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let S be non empty Subset-Family of X; :: thesis: for F, G being Function of NAT ,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let F, G be Function of NAT ,S; :: thesis: for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let A be Element of S; :: 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))
thus union (rng G) c= A /\ (union (rng F)) :: according to XBOOLE_0:def 10 :: thesis: A /\ (union (rng F)) c= union (rng G)

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in union (rng G) or 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 set such that
A4: s in dom G and
A5: E = G . s by A3, FUNCT_1:def 5;
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:6;
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;

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