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 object ; :: 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 and
A4: E in rng G by TARSKI:def 4;
consider s being object such that
A5: s in dom G and
A6: E = G . s by A4, FUNCT_1:def 3;
reconsider s = s as Element of NAT by A5;
A7: r in A /\ (F . s) by A2, A3, A5, A6;
then A8: r in F . s by XBOOLE_0:def 4;
F . s in rng F by A1, A5, FUNCT_1:3;
then A9: r in union (rng F) by A8, TARSKI:def 4;
r in A by A7, XBOOLE_0:def 4;
hence r in A /\ (union (rng F)) by A9, XBOOLE_0:def 4; :: thesis: verum
end;
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in A /\ (union (rng F)) or 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;
A /\ E = G . s by A1, A2, A14, A15;
then A16: r in G . s by A11, A12, XBOOLE_0:def 4;
G . s in rng G by A1, A14, FUNCT_1:3;
hence r in union (rng G) by A16, TARSKI:def 4; :: thesis: verum