let f1, f2 be FinSequence; ex f being FinSequence st
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
A0:
for k being Nat st k in Seg ((len f1) * (len f2)) holds
( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )
by Lem10;
defpred S1[ Nat, object ] means $2 = (f1 . ((($1 -' 1) div (len f2)) + 1)) /\ (f2 . ((($1 -' 1) mod (len f2)) + 1));
A1:
for k being Nat st k in Seg ((len f1) * (len f2)) holds
ex x being object st S1[k,x]
;
consider f being FinSequence such that
A8:
( dom f = Seg ((len f1) * (len f2)) & ( for k being Nat st k in Seg ((len f1) * (len f2)) holds
S1[k,f . k] ) )
from FINSEQ_1:sch 1(A1);
take
f
; ( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
now for x being object st x in (Union f1) /\ (Union f2) holds
x in Union flet x be
object ;
( x in (Union f1) /\ (Union f2) implies x in Union f )assume
x in (Union f1) /\ (Union f2)
;
x in Union fthen A9:
(
x in union (rng f1) &
x in union (rng f2) )
by XBOOLE_0:def 4;
then consider F1 being
set such that A10:
(
x in F1 &
F1 in rng f1 )
by TARSKI:def 4;
consider F2 being
set such that A11:
(
x in F2 &
F2 in rng f2 )
by A9, TARSKI:def 4;
consider i being
object such that A12:
(
i in dom f1 &
F1 = f1 . i )
by A10, FUNCT_1:def 3;
reconsider i =
i as
Nat by A12;
consider j being
object such that A13:
(
j in dom f2 &
F2 = f2 . j )
by A11, FUNCT_1:def 3;
reconsider j =
j as
Nat by A13;
set k =
((len f2) * (i -' 1)) + j;
E4:
( 1
<= i &
i <= len f1 & 1
<= j &
j <= len f2 )
by A12, A13, FINSEQ_3:25;
then F5:
1
<= ((len f2) * (i -' 1)) + j
by NAT_1:12;
(((len f2) * (i -' 1)) + j) -' 1
= (((len f2) * (i -' 1)) + j) - 1
by E4, NAT_D:37;
then E5:
(((len f2) * (i -' 1)) + j) -' 1
= ((len f2) * (i -' 1)) + (j - 1)
;
E7:
(
i - 1
= i -' 1 &
j - 1
= j -' 1 )
by E4, XREAL_1:48, XREAL_0:def 2;
then E8:
((((len f2) * (i -' 1)) + j) -' 1) div (len f2) = ((j -' 1) div (len f2)) + (i -' 1)
by E4, E5, NAT_D:61;
j -' 1
< j
by E7, XREAL_1:44;
then F0:
j -' 1
< len f2
by E4, XXREAL_0:2;
then
(j -' 1) div (len f2) = 0
by NAT_D:27;
then F1:
F1 = f1 . ((((((len f2) * (i -' 1)) + j) -' 1) div (len f2)) + 1)
by A12, E7, E8;
((((len f2) * (i -' 1)) + j) -' 1) mod (len f2) = (j -' 1) mod (len f2)
by E5, E7, NAT_D:61;
then
((((len f2) * (i -' 1)) + j) -' 1) mod (len f2) = j -' 1
by F0, NAT_D:24;
then F3:
F2 = f2 . ((((((len f2) * (i -' 1)) + j) -' 1) mod (len f2)) + 1)
by A13, E7;
i -' 1
<= (len f1) - 1
by E4, E7, XREAL_1:9;
then
(i -' 1) * (len f2) <= ((len f1) - 1) * (len f2)
by XREAL_1:66;
then
((len f2) * (i -' 1)) + j <= (((len f1) - 1) * (len f2)) + (len f2)
by E4, XREAL_1:7;
then F4:
((len f2) * (i -' 1)) + j in Seg ((len f1) * (len f2))
by F5;
then
f . (((len f2) * (i -' 1)) + j) = F1 /\ F2
by A8, F1, F3;
then
(
x in f . (((len f2) * (i -' 1)) + j) &
f . (((len f2) * (i -' 1)) + j) in rng f )
by A10, A11, F4, A8, FUNCT_1:3, XBOOLE_0:def 4;
hence
x in Union f
by TARSKI:def 4;
verum end;
then P1:
(Union f1) /\ (Union f2) c= Union f
;
then
Union f c= (Union f1) /\ (Union f2)
;
hence
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
by A8, P1; verum