let DX1, DX2 be non empty set ; :: thesis:
let F1 be Function of DX1,REAL ; :: thesis:
let F2 be Function of DX2,REAL ; :: thesis:
let G be Function of [:DX1,DX2:],REAL ; :: thesis:
let Y1 be non empty finite Subset of DX1; :: thesis:
let p1 be FinSequence of DX1; :: thesis:
assume AS01: ( p1 is one-to-one & rng p1 = Y1 ) ; :: thesis:
defpred S₁[ Nat] means for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st len p2 = $1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq G,p3) = (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p2));
consider erp1 being set such that
XP1: erp1 in rng p1 by XBOOLE_0:def 1, AS01;
CXDP11: ex x being set st
( x in dom p1 & erp1 = p1 . x ) by FUNCT_1:def 5, XP1;
PP0: S₁[ 0 ]

proof

end;

PPF1: S₁[1]

proof

let p2 be FinSequence of DX2; :: thesis:
let p3 be FinSequence of [:DX1,DX2:]; :: thesis:
let Y2 be non empty finite Subset of DX2; :: thesis:
let Y3 be finite Subset of [:DX1,DX2:]; :: thesis:
assume AS: ( len p2 = 1 & p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) ) ; :: thesis:
then CP2001: p2 = <*(p2 . 1)*> by FINSEQ_1:57;
then CY2: Y2 = {(p2 . 1)} by FINSEQ_1:55, AS;
set w = p2 . 1;
set z = (F2 * p2) . 1;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2 ;
then dom (F2 * p2) = dom p2 by RELAT_1:46;
then CY3: dom (F2 * p2) = Seg 1 by CP2001, FINSEQ_1:55;
then Func_Seq F2,p2 = <*((F2 * p2) . 1)*> by THL1FS2;
then X1: Sum (Func_Seq F2,p2) = (F2 * p2) . 1 by RVSUM_1:103;
X2: Y3 = [:Y1,{(p2 . 1)}:] by AS, CP2001, FINSEQ_1:55;
C1: len p1 = card Y1 by FINSEQ_4:77, AS01;
C2: len p3 = card (rng p3) by FINSEQ_4:77, AS
.= card Y1 by X2, CARD_2:13, AS ;
AAA: dom p1 = Seg (card Y1) by C1, FINSEQ_1:def 3
.= dom p3 by C2, FINSEQ_1:def 3 ;
deffunc H₁( Nat) -> set = [(p1 . $1),(p2 . 1)];
consider q3 being FinSequence such that
X21: len q3 = len p3 and
X22: for k being Nat st k in dom q3 holds
q3 . k = H₁(k) from FINSEQ_1:sch 2();
A14: dom q3 = Seg (len p3) by X21, FINSEQ_1:def 3;
A15: dom p3 = Seg (len p3) by FINSEQ_1:def 3;

now

let k be Nat; :: thesis:
assume A16: k in dom q3 ; :: thesis:
then A24: p1 . k in Y1 by AS01, FUNCT_1:12, A14, A15, AAA;
p2 . 1 in Y2 by TARSKI:def 1, CY2;
then [(p1 . k),(p2 . 1)] in [:Y1,Y2:] by ZFMISC_1:106, A24;
hence q3 . k in [:Y1,Y2:] by A16, X22; :: thesis:

end;

then q3 is FinSequence of [:Y1,Y2:] by FINSEQ_2:14;
then X9: rng q3 c= [:Y1,Y2:] by FINSEQ_1:def 4;
[:Y1,Y2:] c= [:DX1,DX2:] by ZFMISC_1:119;
then rng q3 c= [:DX1,DX2:] by X9, XBOOLE_1:1;
then reconsider q3 = q3 as FinSequence of [:DX1,DX2:] by FINSEQ_1:def 4;

now

let x1, x2 be set ; :: thesis:
assume AD1: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; :: thesis:
then AD1a: ( x1 in dom p1 & x2 in dom p1 ) by X21, FINSEQ_1:def 3, A15, AAA;
reconsider n1 = x1, n2 = x2 as Element of NAT by AD1;
[(p1 . n1),(p2 . 1)] = q3 . n1 by X22, AD1
.= [(p1 . n2),(p2 . 1)] by X22, AD1 ;
then p1 . n1 = p1 . n2 by ZFMISC_1:33;
hence x1 = x2 by AS01, AD1a, FUNCT_1:def 8; :: thesis:

end;

then XJ0: q3 is one-to-one by FUNCT_1:def 8;
XJ1: rng q3 = [:Y1,Y2:]

proof

now

let z be set ; :: thesis:
assume z in [:Y1,Y2:] ; :: thesis:
then consider y1, y2 being set such that
J11: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being set such that
J22: ( n1 in dom p1 & y1 = p1 . n1 ) by AS01, J11, FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by J22;
J25: n1 in dom q3 by J22, X21, FINSEQ_1:def 3, A15, AAA;
y2 = p2 . 1 by CY2, TARSKI:def 1, J11;
then q3 . n1 = z by J11, J22, X22, J25;
hence z in rng q3 by FUNCT_1:12, J25; :: thesis:

end;

then [:Y1,Y2:] c= rng q3 by TARSKI:def 3;
hence rng q3 = [:Y1,Y2:] by X9, XBOOLE_0:def 10; :: thesis:

end;

then consider P being Permutation of (dom p3) such that
H11: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by XJ0, BHSP_5:1, AS;
H13: Func_Seq G,q3 = (Func_Seq G,p3) * P by RELAT_1:55, H11;
dom G = [:DX1,DX2:] by FUNCT_2:def 1;
then rng p3 c= dom G ;
then dom (Func_Seq G,p3) = dom p3 by RELAT_1:46;
then X5: Sum (Func_Seq G,q3) = Sum (Func_Seq G,p3) by H13, FINSOP_1:8;
XXX: dom G = [:DX1,DX2:] by FUNCT_2:def 1;
dom F1 = DX1 by FUNCT_2:def 1;
then XV12: dom (F1 * p1) = dom p1 by RELAT_1:46, AS01
.= Seg (len p1) by FINSEQ_1:def 3 ;
XV3: dom (G * q3) = dom q3 by XXX, XJ1, RELAT_1:46
.= Seg (len p1) by C1, C2, X21, FINSEQ_1:def 3 ;
then XV7: dom (G * q3) = dom (((F2 * p2) . 1) (#) (F1 * p1)) by VALUED_1:def 5, XV12;

now

let x be set ; :: thesis:
assume XV4: x in dom (G * q3) ; :: thesis:
then reconsider nx = x as Element of NAT ;
dom (G * q3) = dom q3 by XXX, XJ1, RELAT_1:46
.= Seg (len q3) by FINSEQ_1:def 3 ;
then J22: nx in dom q3 by FINSEQ_1:def 3, XV4;
( 1 <= nx & nx <= len p1 ) by FINSEQ_1:3, XV4, XV3;
then H3333: p1 /. nx = p1 . nx by FINSEQ_4:24;
XV9003: q3 . nx = [(p1 . nx),(p2 . 1)] by X22, J22;
U3: nx in dom p1 by XV4, XV3, FINSEQ_1:def 3;
then XV9: q3 . nx = [(p1 /. nx),(p2 . 1)] by XV9003, PARTFUN1:def 8;
p1 . nx in Y1 by U3, FUNCT_1:12, AS01;
then test: ( p1 /. nx in Y1 & p2 . 1 in Y2 ) by U3, PARTFUN1:def 8, CY2, TARSKI:def 1;
1 in dom (F2 * p2) by CY3;
then test1: (F2 * p2) . 1 = F2 . (p2 . 1) by FUNCT_1:22;
thus (G * q3) . x = G . (p1 /. nx),(p2 . 1) by XV9, XV4, FUNCT_1:22
.= (F1 . (p1 /. nx)) * ((F2 * p2) . 1) by test1, AS, test
.= ((F1 * p1) . nx) * ((F2 * p2) . 1) by H3333, XV3, XV12, XV4, FUNCT_1:22
.= (((F2 * p2) . 1) (#) (F1 * p1)) . x by VALUED_1:6 ; :: thesis:

end;

then Func_Seq G,q3 = ((F2 * p2) . 1) * (Func_Seq F1,p1) by XV7, FUNCT_1:9;
hence Sum (Func_Seq G,p3) = (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p2)) by X1, X5, RVSUM_1:117; :: thesis:

end;

PP1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A1: S₁[n] ; :: thesis:

now

per cases ;

case n = 0 ; :: thesis:

hence S₁[n + 1] by PPF1; :: thesis:

end;

case CASENNE: n > 0 ; :: thesis:

now

AAA: now

reconsider lap = len p2, lbp = len p1 as natural number ;
let k be Nat; :: thesis:
set i = ((k -' 1) div (len p1)) + 1;
set j = ((k -' 1) mod (len p1)) + 1;
assume k in dom FG ; :: thesis:
then A17: k in Seg ((len p2) * (len p1)) by A12, FINSEQ_1:def 3;
then A18: k <= (len p2) * (len p1) by FINSEQ_1:3;
then k -' 1 <= ((len p2) * (len p1)) -' 1 by NAT_D:42;
then A19: (k -' 1) div (len p1) <= (((len p2) * (len p1)) -' 1) div (len p1) by NAT_2:26;
1 <= k by A17, FINSEQ_1:3;
then A20: ( lbp divides lap * lbp & 1 <= (len p2) * (len p1) ) by A18, NAT_D:def 3, XXREAL_0:2;
A21: len p1 <> 0 by A17;
then len p1 >= 0 + 1 by NAT_1:13;
then ((lap * lbp) -' 1) div lbp = ((lap * lbp) div lbp) - 1 by A20, NAT_2:17;
then A22: ((k -' 1) div (len p1)) + 1 <= ((len p2) * (len p1)) div (len p1) by A19, XREAL_1:21;
reconsider la = len p2, lb = len p1 as Nat ;
( ((k -' 1) div (len p1)) + 1 >= 0 + 1 & ((k -' 1) div (len p1)) + 1 <= la ) by A21, A22, NAT_D:18, XREAL_1:8;
then ((k -' 1) div (len p1)) + 1 in Seg la ;
hence ((k -' 1) div (len p1)) + 1 in dom p2 by FINSEQ_1:def 3; :: thesis:
(k -' 1) mod lb < lb by A21, NAT_D:1;
then ( ((k -' 1) mod (len p1)) + 1 >= 0 + 1 & ((k -' 1) mod (len p1)) + 1 <= lb ) by NAT_1:13;
then ((k -' 1) mod (len p1)) + 1 in Seg lb ;
hence ((k -' 1) mod (len p1)) + 1 in dom p1 by FINSEQ_1:def 3; :: thesis:

end;

now

let k be Nat; :: thesis:
set i = ((k -' 1) div (len p1)) + 1;
set j = ((k -' 1) mod (len p1)) + 1;
assume A16: k in dom FG ; :: thesis:
then A23: p2 . (((k -' 1) div (len p1)) + 1) in rng p2 by FUNCT_1:12, AAA;
p1 . (((k -' 1) mod (len p1)) + 1) in rng p1 by FUNCT_1:12, AAA, A16;
then [(p1 . (((k -' 1) mod (len p1)) + 1)),(p2 . (((k -' 1) div (len p1)) + 1))] in [:DX1,DX2:] by A23, ZFMISC_1:106;
hence FG . k in [:DX1,DX2:] by A13, A16; :: thesis:

end;

then reconsider q3 = FG as FinSequence of [:DX1,DX2:] by FINSEQ_2:14;
LENP1AA: len p1 = card Y1 by AS01, FINSEQ_4:77;

now

let x1, x2 be set ; :: thesis:
assume AD1: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; :: thesis:
then AD1a: ( x1 in Seg (len q3) & x2 in Seg (len q3) ) by FINSEQ_1:def 3;
reconsider n1 = x1, n2 = x2 as Element of NAT by AD1;
AD2: q3 . n1 = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A13, AD1;
AD3: q3 . n2 = [(p1 . (((n2 -' 1) mod (len p1)) + 1)),(p2 . (((n2 -' 1) div (len p1)) + 1))] by A13, AD1;
then AD4: p1 . (((n1 -' 1) mod (len p1)) + 1) = p1 . (((n2 -' 1) mod (len p1)) + 1) by ZFMISC_1:33, AD1, AD2;
( ((n1 -' 1) mod (len p1)) + 1 in dom p1 & ((n2 -' 1) mod (len p1)) + 1 in dom p1 ) by AD1, AAA;
then AD5P: ((n1 -' 1) mod (len p1)) + 1 = ((n2 -' 1) mod (len p1)) + 1 by AS01, AD4, FUNCT_1:def 8;
AD6: p2 . (((n1 -' 1) div (len p1)) + 1) = p2 . (((n2 -' 1) div (len p1)) + 1) by ZFMISC_1:33, AD1, AD2, AD3;
( ((n1 -' 1) div (len p1)) + 1 in dom p2 & ((n2 -' 1) div (len p1)) + 1 in dom p2 ) by AD1, AAA;
then AD7P: ((n1 -' 1) div (len p1)) + 1 = ((n2 -' 1) div (len p1)) + 1 by AS1, AD6, FUNCT_1:def 8;
n1 = n2

proof

X1: ( 1 <= n1 & n1 <= len q3 ) by FINSEQ_1:3, AD1a;
X2: ( 1 <= n2 & n2 <= len q3 ) by FINSEQ_1:3, AD1a;
0 < len p1 by A15, CXDP11;
then X3P: ( n1 -' 1 = ((len p1) * ((n1 -' 1) div (len p1))) + ((n1 -' 1) mod (len p1)) & n2 -' 1 = ((len p1) * ((n1 -' 1) div (len p1))) + ((n1 -' 1) mod (len p1)) ) by AD5P, AD7P, NAT_D:2;
X4: (n1 -' 1) + 1 = (n1 + 1) -' 1 by NAT_D:38, X1
.= n1 by NAT_D:34 ;
(n2 -' 1) + 1 = (n2 + 1) -' 1 by NAT_D:38, X2
.= n2 by NAT_D:34 ;
hence n1 = n2 by X3P, X4; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then J0: q3 is one-to-one by FUNCT_1:def 8;
J1: rng q3 = [:Y1,Y2:]

proof

now

let z be set ; :: thesis:
assume z in [:Y1,Y2:] ; :: thesis:
then consider y1, y2 being set such that
J11: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being set such that
J22: ( n1 in dom p1 & y1 = p1 . n1 ) by AS01, J11, FUNCT_1:def 5;
J22A: n1 in Seg (len p1) by FINSEQ_1:def 3, J22;
reconsider n1 = n1 as Element of NAT by J22;
consider n2 being set such that
J23: ( n2 in dom p2 & y2 = p2 . n2 ) by AS1, J11, FUNCT_1:def 5;
J23A: n2 in Seg (len p2) by FINSEQ_1:def 3, J23;
reconsider n2 = n2 as Element of NAT by J23;
J24A: ( 1 <= n1 & n1 <= len p1 ) by J22A, FINSEQ_1:3;
J24B: ( 1 <= n2 & n2 <= len p2 ) by J23A, FINSEQ_1:3;
reconsider n11 = n1 - 1 as Element of NAT by INT_1:18, J24A;
reconsider n21 = n2 - 1 as Element of NAT by INT_1:18, J24B;
set k1 = n11 + ((len p1) * n21);
J25A: n11 <= (len p1) - 1 by J24A, XREAL_1:11;
(len p1) - 1 < len p1 by XREAL_1:46;
then J26A: n11 < len p1 by J25A, XXREAL_0:2;
J27A: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by LENP1AA, INT_3:8
.= 0 + n21 by J26A, NAT_D:27
.= n21 ;
J27B: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by INT_3:8
.= n11 by J26A, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
J24C: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
J24D: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by XREAL_1:235, NAT_1:14
.= n11 + ((len p1) * n21) ;
then J24E: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by J27B;
J24F: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by J24D, J27A;
J24G: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by XREAL_1:8, J24A;
n21 <= (len p2) - 1 by J24B, XREAL_1:11;
then (len p1) * n21 <= (len p1) * ((len p2) - 1) by XREAL_1:66;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p2) - 1)) by XREAL_1:8;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * (len p2) by J24G, XXREAL_0:2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len FG) by A12, J24C;
then J25: (n11 + ((len p1) * n21)) + 1 in dom FG by FINSEQ_1:def 3;
then q3 . ((n11 + ((len p1) * n21)) + 1) = z by J11, J22, J23, A13, J24E, J24F;
hence z in rng q3 by FUNCT_1:12, J25; :: thesis:

end;

then L1: [:Y1,Y2:] c= rng q3 by TARSKI:def 3;

now

let z be set ; :: thesis:
assume z in rng q3 ; :: thesis:
then consider n1 being set such that
J22: ( n1 in dom q3 & z = q3 . n1 ) by FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by J22;
J28: z = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by J22, A13;
J23: p1 . (((n1 -' 1) mod (len p1)) + 1) in Y1 by AS01, FUNCT_1:12, J22, AAA;
((n1 -' 1) div (len p1)) + 1 in dom p2 by J22, AAA;
then p2 . (((n1 -' 1) div (len p1)) + 1) in Y2 by AS1, FUNCT_1:12;
hence z in [:Y1,Y2:] by J28, J23, ZFMISC_1:def 2; :: thesis:

end;

then rng q3 c= [:Y1,Y2:] by TARSKI:def 3;
hence rng q3 = [:Y1,Y2:] by L1, XBOOLE_0:def 10; :: thesis:

end;

set q30 = q3 | ((len p1) * n);
(len p1) * n <= (len p1) * (len p2) by XREAL_1:66, NAT_1:11, AS1;
then LENQ30: len (q3 | ((len p1) * n)) = (len p1) * n by FINSEQ_1:21, A12;
set q31 = q3 /^ ((len p1) * n);
reconsider q30 = q3 | ((len p1) * n) as FinSequence of [:DX1,DX2:] ;
reconsider q31 = q3 /^ ((len p1) * n) as FinSequence of [:DX1,DX2:] ;
reconsider nn = (len p1) * n as Nat ;
H0: q3 = q30 ^ q31 by RFINSEQ:21;
set p20 = p2 | n;
reconsider p20 = p2 | n as FinSequence of DX2 ;
XX2: len p20 = n by FINSEQ_3:59, AS1;
then XX3: not dom p20 is empty by CASENNE, FINSEQ_1:def 3;
H1: p20 is one-to-one by FUNCT_1:84, AS1;
reconsider Y20 = rng p20 as non empty finite Subset of DX2 by XX3, RELAT_1:65;
H3: q30 is one-to-one by J0, FUNCT_1:84;
H4: rng q30 = [:Y1,Y20:]

proof

now

let z be set ; :: thesis:
assume z in [:Y1,Y20:] ; :: thesis:
then consider y1, y2 being set such that
J11: ( y1 in Y1 & y2 in Y20 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being set such that
J22: ( n1 in dom p1 & y1 = p1 . n1 ) by AS01, J11, FUNCT_1:def 5;
J22A: n1 in Seg (len p1) by FINSEQ_1:def 3, J22;
reconsider n1 = n1 as Element of NAT by J22;
consider n2 being set such that
J23: ( n2 in dom p20 & y2 = p20 . n2 ) by J11, FUNCT_1:def 5;
J23A: n2 in Seg (len p20) by FINSEQ_1:def 3, J23;
reconsider n2 = n2 as Element of NAT by J23;
J230: y2 = p2 . n2 by J23, FUNCT_1:70;
J24A: ( 1 <= n1 & n1 <= len p1 ) by J22A, FINSEQ_1:3;
J24B: ( 1 <= n2 & n2 <= len p20 ) by J23A, FINSEQ_1:3;
reconsider n11 = n1 - 1 as Element of NAT by INT_1:18, J24A;
reconsider n21 = n2 - 1 as Element of NAT by INT_1:18, J24B;
set k1 = n11 + ((len p1) * n21);
J25A: n11 <= (len p1) - 1 by J24A, XREAL_1:11;
(len p1) - 1 < len p1 by XREAL_1:46;
then J26A: n11 < len p1 by J25A, XXREAL_0:2;
J27A: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by LENP1AA, INT_3:8
.= 0 + n21 by J26A, NAT_D:27
.= n21 ;
J27B: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by INT_3:8
.= n11 by J26A, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
J24C: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
J24D: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by XREAL_1:235, NAT_1:14
.= n11 + ((len p1) * n21) ;
then J24E: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by J27B;
J24F: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by J24D, J27A;
J24G: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by XREAL_1:8, J24A;
n21 <= (len p20) - 1 by J24B, XREAL_1:11;
then (len p1) * n21 <= (len p1) * ((len p20) - 1) by XREAL_1:66;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p20) - 1)) by XREAL_1:8;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * n by J24G, XXREAL_0:2, XX2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len q30) by J24C, LENQ30;
then J25: (n11 + ((len p1) * n21)) + 1 in dom q30 by FINSEQ_1:def 3;
then J250: (n11 + ((len p1) * n21)) + 1 in dom q3 by RELAT_1:86;
q30 . ((n11 + ((len p1) * n21)) + 1) = q3 . ((n11 + ((len p1) * n21)) + 1) by J25, FUNCT_1:70
.= z by J11, J22, J230, A13, J250, J24E, J24F ;
hence z in rng q30 by FUNCT_1:12, J25; :: thesis:

end;

then L1: [:Y1,Y20:] c= rng q30 by TARSKI:def 3;

now

end;

then rng q30 c= [:Y1,Y20:] by TARSKI:def 3;
hence rng q30 = [:Y1,Y20:] by L1, XBOOLE_0:def 10; :: thesis:

end;

then reconsider Y30 = [:Y1,Y20:] as non empty finite Subset of [:DX1,DX2:] ;

now

let x, y be set ; :: thesis:
assume H51: ( x in Y1 & y in Y20 ) ; :: thesis:
Y20 c= rng p2 by RELAT_1:99;
hence G . x,y = (F1 . x) * (F2 . y) by AS1, H51; :: thesis:

end;

then H6: Sum (Func_Seq G,q30) = (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p20)) by A1, H1, H3, H4, XX2;
dom F1 = DX1 by FUNCT_2:def 1;
then XV12: dom (F1 * p1) = dom p1 by RELAT_1:46, AS01
.= Seg (len p1) by FINSEQ_1:def 3 ;
DDD1: dom G = [:DX1,DX2:] by FUNCT_2:def 1;
len q3 = (n * (len p1)) + (len p1) by AS1, A12;
then HH011: n * (len p1) <= len q3 by NAT_1:11;
then HH02: len q31 = (len q3) - ((len p1) * n) by RFINSEQ:def 2
.= len p1 by AS1, A12 ;
XV3P: ( [:Y1,Y2:] c= [:DX1,DX2:] & rng q31 c= rng q3 ) by AS1, FINSEQ_5:36;
then XV3: dom (G * q31) = dom q31 by DDD1, RELAT_1:46
.= Seg (len p1) by HH02, FINSEQ_1:def 3 ;
then XV7: dom (G * q31) = dom (((Func_Seq F2,p2) /. (n + 1)) (#) (F1 * p1)) by XV12, VALUED_1:def 5;

now

let x be set ; :: thesis:
assume XV4: x in dom (G * q31) ; :: thesis:
then reconsider nx = x as Element of NAT ;
J22NXP: dom (G * q31) = dom q31 by DDD1, RELAT_1:46, XV3P
.= Seg (len q31) by FINSEQ_1:def 3 ;
UU1: ( 1 <= nx & nx <= len p1 ) by FINSEQ_1:3, XV4, XV3;
then H3333: p1 /. nx = p1 . nx by FINSEQ_4:24;
H3344: ( 1 <= n + 1 & n + 1 <= len p2 ) by AS1, XREAL_1:33;
then U2: n + 1 in Seg (len p2) ;
then H4433: n + 1 in dom p2 by FINSEQ_1:def 3;
H3344a: p2 /. (n + 1) = p2 . (n + 1) by FINSEQ_4:24, H3344;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2 ;
then H44332: n + 1 in dom (F2 * p2) by H4433, RELAT_1:46;
H4444: F2 . (p2 /. (n + 1)) = (F2 * p2) . (n + 1) by H4433, FUNCT_1:23, H3344a
.= (Func_Seq F2,p2) /. (n + 1) by PARTFUN1:def 8, H44332 ;
XLLL1: ( 1 <= nx & nx <= len p1 ) by FINSEQ_1:3, J22NXP, XV4, HH02;
then XLLL2P: nx + ((len p1) * n) <= (len p1) + ((len p1) * n) by XREAL_1:8;
XV800P: nx <= nx + ((len p1) * n) by NAT_1:11;
then ( 1 <= nx + ((len p1) * n) & nx + ((len p1) * n) <= (len p1) * (len p2) ) by XLLL2P, AS1, XXREAL_0:2, XLLL1;
then nx + ((len p1) * n) in dom FG by A14;
then XV9005: q3 . (nx + ((len p1) * n)) = [(p1 . ((((nx + ((len p1) * n)) -' 1) mod (len p1)) + 1)),(p2 . ((((nx + ((len p1) * n)) -' 1) div (len p1)) + 1))] by A13;
XV9000P: nx in dom q31 by J22NXP, XV4, FINSEQ_1:def 3;
XV7001: (nx + ((len p1) * n)) -' 1 = (nx + ((len p1) * n)) - 1 by XV800P, XXREAL_0:2, XLLL1, XREAL_1:235
.= (nx - 1) + ((len p1) * n)
.= (nx -' 1) + ((len p1) * n) by UU1, XREAL_1:235 ;
nx - 1 < nx by XREAL_1:46;
then nx - 1 < len p1 by XLLL1, XXREAL_0:2;
then XV7002: nx -' 1 < len p1 by UU1, XREAL_1:235;
XVX: (((nx -' 1) + ((len p1) * n)) div (len p1)) + 1 = (((nx -' 1) div (len p1)) + n) + 1 by LENP1AA, INT_3:8
.= (0 + n) + 1 by XV7002, NAT_D:27 ;
XV93P: (((nx -' 1) + ((len p1) * n)) mod (len p1)) + 1 = ((nx -' 1) mod (len p1)) + 1 by INT_3:8
.= (nx -' 1) + 1 by XV7002, NAT_D:24
.= (nx - 1) + 1 by UU1, XREAL_1:235 ;
U3: ( nx in dom p1 & n + 1 in dom p2 ) by XV4, XV3, U2, FINSEQ_1:def 3;
then ( p1 /. nx = p1 . nx & p2 . (n + 1) = p2 /. (n + 1) ) by PARTFUN1:def 8;
then XV9: q31 . nx = [(p1 /. nx),(p2 /. (n + 1))] by XV9000P, XV9005, RFINSEQ:def 2, HH011, XV7001, XVX, XV93P;
( p1 . nx in Y1 & p2 . (n + 1) in Y2 ) by U3, FUNCT_1:12, AS1, AS01;
then test: ( p1 /. nx in Y1 & p2 /. (n + 1) in Y2 ) by U3, PARTFUN1:def 8;
thus (G * q31) . x = G . (p1 /. nx),(p2 /. (n + 1)) by XV9, XV4, FUNCT_1:22
.= (F1 . (p1 /. nx)) * (F2 . (p2 /. (n + 1))) by AS1, test
.= ((F1 * p1) . nx) * ((Func_Seq F2,p2) /. (n + 1)) by H4444, H3333, XV12, XV4, XV3, FUNCT_1:22
.= (((Func_Seq F2,p2) /. (n + 1)) (#) (F1 * p1)) . x by VALUED_1:6 ; :: thesis:

end;

then Func_Seq G,q31 = ((Func_Seq F2,p2) /. (n + 1)) * (Func_Seq F1,p1) by XV7, FUNCT_1:9;
then H7: Sum (Func_Seq G,q31) = (Sum (Func_Seq F1,p1)) * ((Func_Seq F2,p2) /. (n + 1)) by RVSUM_1:117;
H8: Func_Seq G,q3 = (Func_Seq G,q30) ^ (Func_Seq G,q31) by H0, LMXXX1;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2 ;
then dom (F2 * p2) = dom p2 by RELAT_1:46;
then dom (Func_Seq F2,p2) = Seg (len p2) by FINSEQ_1:def 3;
then H90: len (Func_Seq F2,p2) = n + 1 by AS1, FINSEQ_1:def 3;
(Func_Seq F2,p2) | n = Func_Seq F2,p20 by RELAT_1:112;
then H9: Func_Seq F2,p2 = (Func_Seq F2,p20) ^ <*((Func_Seq F2,p2) /. (n + 1))*> by FINSEQ_5:24, H90;
H10: Sum (Func_Seq G,q3) = (Sum (Func_Seq G,q30)) + (Sum (Func_Seq G,q31)) by RVSUM_1:105, H8
.= (Sum (Func_Seq F1,p1)) * ((Sum (Func_Seq F2,p20)) + ((Func_Seq F2,p2) /. (n + 1))) by H6, H7
.= (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p2)) by RVSUM_1:104, H9 ;
consider P being Permutation of (dom p3) such that
H11: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by J0, J1, BHSP_5:1, AS1;
H13: Func_Seq G,q3 = (Func_Seq G,p3) * P by RELAT_1:55, H11;
dom G = [:DX1,DX2:] by FUNCT_2:def 1;
then rng p3 c= dom G ;
then dom (Func_Seq G,p3) = dom p3 by RELAT_1:46;
hence Sum (Func_Seq G,p3) = (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p2)) by H10, H13, FINSOP_1:8; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

L1: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(PP0, PP1);

now

end;

hence for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq G,p3) = (Sum (Func_Seq F1,p1)) * (Sum (Func_Seq F2,p2)) ; :: thesis: