let X be non empty set ; :: thesis: for A being set
for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
let A be set ; :: thesis: for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
let F, G be FinSequence of X; :: thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) implies union (rng G) = A /\ (union (rng F)) )
assume that
A1: dom G = dom F and
A2: for i being Nat st i in dom G holds
G . i = A /\ (F . i) ; :: 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
A3: ( r in E & E in rng G ) by TARSKI:def 4;
consider s being set such that
A4: ( s in dom G & E = G . s ) by A3, FUNCT_1:def 5;
reconsider s = s as Element of NAT by A4;
r in A /\ (F . s) by A2, A3, A4;
then A5: ( r in A & r in F . s ) by XBOOLE_0:def 4;
F . s in rng F by A1, A4, FUNCT_1:12;
then r in union (rng F) by A5, TARSKI:def 4;
hence r in A /\ (union (rng F)) by A5, 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 r in A /\ (union (rng F)) ; :: thesis: r in union (rng G)
then A6: ( r in A & r in union (rng F) ) by XBOOLE_0:def 4;
then consider E being set such that
A7: ( r in E & E in rng F ) by TARSKI:def 4;
consider s being set such that
A8: ( s in dom F & E = F . s ) by A7, FUNCT_1:def 5;
reconsider s = s as Element of NAT by A8;
A /\ E = G . s by A1, A2, A8;
then A9: r in G . s by A6, A7, XBOOLE_0:def 4;
G . s in rng G by A1, A8, FUNCT_1:12;
hence r in union (rng G) by A9, TARSKI:def 4; :: thesis: verum