let D be non empty set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y holds rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y holds rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }
let F be FinSequence of Y; :: thesis: rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }
now :: thesis: for x being object st x in rng (joined_FinSeq F) holds
x in union { (rng (F . n)) where n is Nat : n in dom F }
let x be object ; :: thesis: ( x in rng (joined_FinSeq F) implies x in union { (rng (F . n)) where n is Nat : n in dom F } )
assume x in rng (joined_FinSeq F) ; :: thesis: x in union { (rng (F . n)) where n is Nat : n in dom F }
then consider n being object such that
A1: ( n in dom (joined_FinSeq F) & x = (joined_FinSeq F) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A1;
consider k, m being Nat such that
A2: ( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & (joined_FinSeq F) . n = (F . (k + 1)) . m ) by A1, Def2;
( 1 <= k + 1 & k + 1 <= len F ) by A2, NAT_1:11, NAT_1:13;
then A3: k + 1 in dom F by FINSEQ_3:25;
m in dom (F . (k + 1)) by A2, FINSEQ_3:25;
then A4: x in rng (F . (k + 1)) by A1, A2, FUNCT_1:3;
rng (F . (k + 1)) in { (rng (F . n)) where n is Nat : n in dom F } by A3;
hence x in union { (rng (F . n)) where n is Nat : n in dom F } by A4, TARSKI:def 4; :: thesis: verum
end;
then A5: rng (joined_FinSeq F) c= union { (rng (F . n)) where n is Nat : n in dom F } by TARSKI:def 3;
now :: thesis: for x being object st x in union { (rng (F . n)) where n is Nat : n in dom F } holds
x in rng (joined_FinSeq F)
let x be object ; :: thesis: ( x in union { (rng (F . n)) where n is Nat : n in dom F } implies x in rng (joined_FinSeq F) )
assume x in union { (rng (F . n)) where n is Nat : n in dom F } ; :: thesis: x in rng (joined_FinSeq F)
then consider A being set such that
A6: ( x in A & A in { (rng (F . n)) where n is Nat : n in dom F } ) by TARSKI:def 4;
consider k being Nat such that
A7: ( A = rng (F . k) & k in dom F ) by A6;
consider m being object such that
A8: ( m in dom (F . k) & x = (F . k) . m ) by A6, A7, FUNCT_1:def 3;
reconsider m = m as Nat by A8;
A9: ( 1 <= k & k <= len F ) by A7, FINSEQ_3:25;
reconsider k1 = k - 1 as Nat by A7, FINSEQ_3:25, NAT_1:21;
set n = m + (Sum (Length (F | k1)));
Length (F | (k1 + 1)) = (Length (F | k1)) ^ <*(len (F . (k1 + 1)))*> by Th2, A9, NAT_1:13;
then A11: Sum (Length (F | (k1 + 1))) = (Sum (Length (F | k1))) + (len (F . (k1 + 1))) by RVSUM_1:74;
A14: ( 1 <= m & m <= len (F . (k1 + 1)) ) by A8, FINSEQ_3:25;
then A12: m + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) by A11, XREAL_1:6;
Sum (Length (F | (k1 + 1))) <= Sum (Length (F | (len F))) by A9, Th5;
then m + (Sum (Length (F | k1))) <= Sum (Length (F | (len F))) by A12, XXREAL_0:2;
then m + (Sum (Length (F | k1))) <= Sum (Length F) by FINSEQ_1:58;
then A13: m + (Sum (Length (F | k1))) <= len (joined_FinSeq F) by Def2;
m <= m + (Sum (Length (F | k1))) by NAT_1:11;
then 1 <= m + (Sum (Length (F | k1))) by A14, XXREAL_0:2;
then A17: m + (Sum (Length (F | k1))) in dom (joined_FinSeq F) by A13, FINSEQ_3:25;
then consider k2, m2 being Nat such that
A15: ( 1 <= m2 & m2 <= len (F . (k2 + 1)) & k2 < len F & m2 + (Sum (Length (F | k2))) = m + (Sum (Length (F | k1))) & m + (Sum (Length (F | k1))) <= Sum (Length (F | (k2 + 1))) & (joined_FinSeq F) . (m + (Sum (Length (F | k1)))) = (F . (k2 + 1)) . m2 ) by Def2;
( m = m2 & k1 = k2 ) by A14, A15, A12, Th6;
hence x in rng (joined_FinSeq F) by A8, A15, A17, FUNCT_1:3; :: thesis: verum
end;
then union { (rng (F . n)) where n is Nat : n in dom F } c= rng (joined_FinSeq F) by TARSKI:def 3;
hence rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F } by A5, XBOOLE_0:def 10; :: thesis: verum