let f1, f2 be FinSequence; :: thesis: 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 S₁[ 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 S₁[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
S₁[k,f . k] ) ) from FINSEQ_1:sch 1(A1);
take f ; :: thesis: ( (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 :: thesis: for x being object st x in (Union f1) /\ (Union f2) holds
x in Union f

let x be object ; :: thesis: ( x in (Union f1) /\ (Union f2) implies x in Union f )
assume x in (Union f1) /\ (Union f2) ; :: thesis: x in Union f
then 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; :: thesis: verum

end;

then P1: (Union f1) /\ (Union f2) c= Union f ;

now :: thesis: for x being object st x in Union f holds
x in (Union f1) /\ (Union f2)

let x be object ; :: thesis: ( x in Union f implies x in (Union f1) /\ (Union f2) )
assume x in Union f ; :: thesis: x in (Union f1) /\ (Union f2)
then consider F being set such that
G1: ( x in F & F in rng f ) by TARSKI:def 4;
consider i being object such that
G2: ( i in dom f & F = f . i ) by G1, FUNCT_1:def 3;
reconsider i = i as Nat by G2;
F = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) by A8, G2;
then G3: ( x in f1 . (((i -' 1) div (len f2)) + 1) & x in f2 . (((i -' 1) mod (len f2)) + 1) ) by G1, XBOOLE_0:def 4;
( f1 . (((i -' 1) div (len f2)) + 1) in rng f1 & f2 . (((i -' 1) mod (len f2)) + 1) in rng f2 ) by G2, A8, A0, FUNCT_1:3;
then ( x in union (rng f1) & x in union (rng f2) ) by G3, TARSKI:def 4;
hence x in (Union f1) /\ (Union f2) by XBOOLE_0:def 4; :: thesis: verum

end;

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; :: thesis: verum