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 A1: ( 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 object such that
A2: erp1 in rng p1 by A1, XBOOLE_0:def 1;
A3: ex x being object st
( x in dom p1 & erp1 = p1 . x ) by A2, FUNCT_1:def 3;
A4: S₁[ 0 ]

proof

end;

A6: 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 A7: ( 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 A8: p2 = <*(p2 . 1)*> by FINSEQ_1:40;
then A9: Y2 = {(p2 . 1)} by A7, FINSEQ_1:38;
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:27;
then A10: dom (F2 * p2) = Seg 1 by A8, FINSEQ_1:38;
then Func_Seq (F2,p2) = <*((F2 * p2) . 1)*> by Lm6;
then A11: Sum (Func_Seq (F2,p2)) = (F2 * p2) . 1 by RVSUM_1:73;
A12: Y3 = [:Y1,{(p2 . 1)}:] by A7, A8, FINSEQ_1:38;
A13: len p1 = card Y1 by A1, FINSEQ_4:62;
A14: len p3 = card (rng p3) by A7, FINSEQ_4:62
.= card Y1 by A12, A7, CARD_1:69 ;
A15: dom p1 = Seg (card Y1) by A13, FINSEQ_1:def 3
.= dom p3 by A14, FINSEQ_1:def 3 ;
deffunc H₁( Nat) -> object = [(p1 . $1),(p2 . 1)];
consider q3 being FinSequence such that
A16: len q3 = len p3 and
A17: for k being Nat st k in dom q3 holds
q3 . k = H₁(k) from FINSEQ_1:sch 2();
A18: dom q3 = Seg (len p3) by A16, FINSEQ_1:def 3;
A19: dom p3 = Seg (len p3) by FINSEQ_1:def 3;

now :: thesis:

let k be Nat; :: thesis:
assume A20: k in dom q3 ; :: thesis:
then A21: p1 . k in Y1 by A1, A18, A19, A15, FUNCT_1:3;
p2 . 1 in Y2 by A9, TARSKI:def 1;
then [(p1 . k),(p2 . 1)] in [:Y1,Y2:] by A21, ZFMISC_1:87;
hence q3 . k in [:Y1,Y2:] by A20, A17; :: thesis:

end;

then q3 is FinSequence of [:Y1,Y2:] by FINSEQ_2:12;
then A22: rng q3 c= [:Y1,Y2:] by FINSEQ_1:def 4;
[:Y1,Y2:] c= [:DX1,DX2:] by ZFMISC_1:96;
then rng q3 c= [:DX1,DX2:] by A22;
then reconsider q3 = q3 as FinSequence of [:DX1,DX2:] by FINSEQ_1:def 4;

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A23: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; :: thesis:
then A24: ( x1 in dom p1 & x2 in dom p1 ) by A16, A19, A15, FINSEQ_1:def 3;
reconsider n1 = x1, n2 = x2 as Element of NAT by A23;
[(p1 . n1),(p2 . 1)] = q3 . n1 by A17, A23
.= [(p1 . n2),(p2 . 1)] by A17, A23 ;
then p1 . n1 = p1 . n2 by XTUPLE_0:1;
hence x1 = x2 by A1, A24, FUNCT_1:def 4; :: thesis:

end;

then A25: q3 is one-to-one by FUNCT_1:def 4;
A26: rng q3 = [:Y1,Y2:]

proof

now :: thesis:

let z be object ; :: thesis:
assume z in [:Y1,Y2:] ; :: thesis:
then consider y1, y2 being object such that
A27: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being object such that
A28: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A27, FUNCT_1:def 3;
reconsider n1 = n1 as Element of NAT by A28;
A29: n1 in dom q3 by A28, A16, A19, A15, FINSEQ_1:def 3;
y2 = p2 . 1 by A9, A27, TARSKI:def 1;
then q3 . n1 = z by A27, A28, A17, A29;
hence z in rng q3 by A29, FUNCT_1:3; :: thesis:

end;

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

end;

then consider P being Permutation of (dom p3) such that
A30: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by A25, A7, BHSP_5:1;
A31: Func_Seq (G,q3) = (Func_Seq (G,p3)) * P by A30, RELAT_1:36;
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:27;
then A32: Sum (Func_Seq (G,q3)) = Sum (Func_Seq (G,p3)) by A31, FINSOP_1:7;
A33: dom G = [:DX1,DX2:] by FUNCT_2:def 1;
dom F1 = DX1 by FUNCT_2:def 1;
then A34: dom (F1 * p1) = dom p1 by A1, RELAT_1:27
.= Seg (len p1) by FINSEQ_1:def 3 ;
A35: dom (G * q3) = dom q3 by A33, A26, RELAT_1:27
.= Seg (len p1) by A13, A14, A16, FINSEQ_1:def 3 ;
then A36: dom (G * q3) = dom (((F2 * p2) . 1) (#) (F1 * p1)) by A34, VALUED_1:def 5;

now :: thesis:

let x be object ; :: thesis:
assume A37: x in dom (G * q3) ; :: thesis:
then reconsider nx = x as Element of NAT ;
dom (G * q3) = dom q3 by A33, A26, RELAT_1:27
.= Seg (len q3) by FINSEQ_1:def 3 ;
then A38: nx in dom q3 by A37, FINSEQ_1:def 3;
( 1 <= nx & nx <= len p1 ) by A37, A35, FINSEQ_1:1;
then A39: p1 /. nx = p1 . nx by FINSEQ_4:15;
A40: q3 . nx = [(p1 . nx),(p2 . 1)] by A17, A38;
A41: nx in dom p1 by A37, A35, FINSEQ_1:def 3;
then A42: q3 . nx = [(p1 /. nx),(p2 . 1)] by A40, PARTFUN1:def 6;
p1 . nx in Y1 by A41, A1, FUNCT_1:3;
then A43: ( p1 /. nx in Y1 & p2 . 1 in Y2 ) by A41, A9, PARTFUN1:def 6, TARSKI:def 1;
1 in dom (F2 * p2) by A10;
then A44: (F2 * p2) . 1 = F2 . (p2 . 1) by FUNCT_1:12;
thus (G * q3) . x = G . ((p1 /. nx),(p2 . 1)) by A42, A37, FUNCT_1:12
.= (F1 . (p1 /. nx)) * ((F2 * p2) . 1) by A44, A7, A43
.= ((F1 * p1) . nx) * ((F2 * p2) . 1) by A39, A35, A34, A37, FUNCT_1:12
.= (((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 A36, FUNCT_1:2;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A11, A32, RVSUM_1:87; :: thesis:

end;

A45: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A46: S₁[n] ; :: thesis:

now :: thesis:

per cases ;

case n = 0 ; :: thesis:

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

end;

case A47: n > 0 ; :: thesis:

now :: thesis:

A53: now :: thesis:

reconsider lap = len p2, lbp = len p1 as Nat ;
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 A54: k in Seg ((len p2) * (len p1)) by A49, FINSEQ_1:def 3;
then A55: k <= (len p2) * (len p1) by FINSEQ_1:1;
then k -' 1 <= ((len p2) * (len p1)) -' 1 by NAT_D:42;
then A56: (k -' 1) div (len p1) <= (((len p2) * (len p1)) -' 1) div (len p1) by NAT_2:24;
1 <= k by A54, FINSEQ_1:1;
then A57: ( lbp divides lap * lbp & 1 <= (len p2) * (len p1) ) by A55, NAT_D:def 3, XXREAL_0:2;
A58: len p1 <> 0 by A54;
then len p1 >= 0 + 1 by NAT_1:13;
then ((lap * lbp) -' 1) div lbp = ((lap * lbp) div lbp) - 1 by A57, NAT_2:15;
then A59: ((k -' 1) div (len p1)) + 1 <= ((len p2) * (len p1)) div (len p1) by A56, XREAL_1:19;
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 A58, A59, NAT_D:18, XREAL_1:6;
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 A58, 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 :: thesis:

let k be Nat; :: thesis:
set i = ((k -' 1) div (len p1)) + 1;
set j = ((k -' 1) mod (len p1)) + 1;
assume A60: k in dom FG ; :: thesis:
then A61: p2 . (((k -' 1) div (len p1)) + 1) in rng p2 by A53, FUNCT_1:3;
p1 . (((k -' 1) mod (len p1)) + 1) in rng p1 by A53, A60, FUNCT_1:3;
then [(p1 . (((k -' 1) mod (len p1)) + 1)),(p2 . (((k -' 1) div (len p1)) + 1))] in [:DX1,DX2:] by A61, ZFMISC_1:87;
hence FG . k in [:DX1,DX2:] by A50, A60; :: thesis:

end;

then reconsider q3 = FG as FinSequence of [:DX1,DX2:] by FINSEQ_2:12;
A62: len p1 = card Y1 by A1, FINSEQ_4:62;

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A63: ( x1 in dom q3 & x2 in dom q3 & q3 . x1 = q3 . x2 ) ; :: thesis:
then A64: ( 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 A63;
A65: q3 . n1 = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A50, A63;
A66: q3 . n2 = [(p1 . (((n2 -' 1) mod (len p1)) + 1)),(p2 . (((n2 -' 1) div (len p1)) + 1))] by A50, A63;
then A67: p1 . (((n1 -' 1) mod (len p1)) + 1) = p1 . (((n2 -' 1) mod (len p1)) + 1) by A63, A65, XTUPLE_0:1;
( ((n1 -' 1) mod (len p1)) + 1 in dom p1 & ((n2 -' 1) mod (len p1)) + 1 in dom p1 ) by A63, A53;
then A68: ((n1 -' 1) mod (len p1)) + 1 = ((n2 -' 1) mod (len p1)) + 1 by A1, A67, FUNCT_1:def 4;
A69: p2 . (((n1 -' 1) div (len p1)) + 1) = p2 . (((n2 -' 1) div (len p1)) + 1) by A63, A65, A66, XTUPLE_0:1;
( ((n1 -' 1) div (len p1)) + 1 in dom p2 & ((n2 -' 1) div (len p1)) + 1 in dom p2 ) by A63, A53;
then A70: ((n1 -' 1) div (len p1)) + 1 = ((n2 -' 1) div (len p1)) + 1 by A48, A69, FUNCT_1:def 4;
n1 = n2

proof

A71: ( 1 <= n1 & n1 <= len q3 ) by A64, FINSEQ_1:1;
A72: ( 1 <= n2 & n2 <= len q3 ) by A64, FINSEQ_1:1;
0 < len p1 by A52, A3;
then A73: ( 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 A68, A70, NAT_D:2;
A74: (n1 -' 1) + 1 = (n1 + 1) -' 1 by A71, NAT_D:38
.= n1 by NAT_D:34 ;
(n2 -' 1) + 1 = (n2 + 1) -' 1 by A72, NAT_D:38
.= n2 by NAT_D:34 ;
hence n1 = n2 by A73, A74; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then A75: q3 is one-to-one by FUNCT_1:def 4;
A76: rng q3 = [:Y1,Y2:]

proof

now :: thesis:

let z be object ; :: thesis:
assume z in [:Y1,Y2:] ; :: thesis:
then consider y1, y2 being object such that
A77: ( y1 in Y1 & y2 in Y2 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being object such that
A78: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A77, FUNCT_1:def 3;
A79: n1 in Seg (len p1) by A78, FINSEQ_1:def 3;
reconsider n1 = n1 as Element of NAT by A78;
consider n2 being object such that
A80: ( n2 in dom p2 & y2 = p2 . n2 ) by A48, A77, FUNCT_1:def 3;
A81: n2 in Seg (len p2) by A80, FINSEQ_1:def 3;
reconsider n2 = n2 as Element of NAT by A80;
A82: ( 1 <= n1 & n1 <= len p1 ) by A79, FINSEQ_1:1;
A83: ( 1 <= n2 & n2 <= len p2 ) by A81, FINSEQ_1:1;
reconsider n11 = n1 - 1 as Element of NAT by A82, INT_1:5;
reconsider n21 = n2 - 1 as Element of NAT by A83, INT_1:5;
set k1 = n11 + ((len p1) * n21);
A84: n11 <= (len p1) - 1 by A82, XREAL_1:9;
(len p1) - 1 < len p1 by XREAL_1:44;
then A85: n11 < len p1 by A84, XXREAL_0:2;
A86: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by A62, NAT_D:61
.= 0 + n21 by A85, NAT_D:27
.= n21 ;
A87: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by NAT_D:61
.= n11 by A85, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
A88: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
A89: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by NAT_1:14, XREAL_1:233
.= n11 + ((len p1) * n21) ;
then A90: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by A87;
A91: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by A89, A86;
A92: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by A82, XREAL_1:6;
n21 <= (len p2) - 1 by A83, XREAL_1:9;
then (len p1) * n21 <= (len p1) * ((len p2) - 1) by XREAL_1:64;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p2) - 1)) by XREAL_1:6;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * (len p2) by A92, XXREAL_0:2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len FG) by A49, A88;
then A93: (n11 + ((len p1) * n21)) + 1 in dom FG by FINSEQ_1:def 3;
then q3 . ((n11 + ((len p1) * n21)) + 1) = z by A77, A78, A80, A50, A90, A91;
hence z in rng q3 by A93, FUNCT_1:3; :: thesis:

end;

then A94: [:Y1,Y2:] c= rng q3 ;

now :: thesis:

let z be object ; :: thesis:
assume z in rng q3 ; :: thesis:
then consider n1 being object such that
A95: ( n1 in dom q3 & z = q3 . n1 ) by FUNCT_1:def 3;
reconsider n1 = n1 as Element of NAT by A95;
A96: z = [(p1 . (((n1 -' 1) mod (len p1)) + 1)),(p2 . (((n1 -' 1) div (len p1)) + 1))] by A95, A50;
A97: p1 . (((n1 -' 1) mod (len p1)) + 1) in Y1 by A1, A95, A53, FUNCT_1:3;
((n1 -' 1) div (len p1)) + 1 in dom p2 by A95, A53;
then p2 . (((n1 -' 1) div (len p1)) + 1) in Y2 by A48, FUNCT_1:3;
hence z in [:Y1,Y2:] by A96, A97, ZFMISC_1:def 2; :: thesis:

end;

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

end;

set q30 = q3 | ((len p1) * n);
(len p1) * n <= (len p1) * (len p2) by A48, NAT_1:11, XREAL_1:64;
then A98: len (q3 | ((len p1) * n)) = (len p1) * n by A49, FINSEQ_1:17;
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:] ;
A99: q3 = q30 ^ q31 by RFINSEQ:8;
set p20 = p2 | n;
reconsider p20 = p2 | n as FinSequence of DX2 ;
A100: len p20 = n by A48, FINSEQ_3:53;
then A101: not dom p20 is empty by A47, FINSEQ_1:def 3;
A102: p20 is one-to-one by A48, FUNCT_1:52;
reconsider Y20 = rng p20 as non empty finite Subset of DX2 by A101, RELAT_1:42;
A103: q30 is one-to-one by A75, FUNCT_1:52;
A104: rng q30 = [:Y1,Y20:]

proof

now :: thesis:

let z be object ; :: thesis:
assume z in [:Y1,Y20:] ; :: thesis:
then consider y1, y2 being object such that
A105: ( y1 in Y1 & y2 in Y20 & z = [y1,y2] ) by ZFMISC_1:def 2;
consider n1 being object such that
A106: ( n1 in dom p1 & y1 = p1 . n1 ) by A1, A105, FUNCT_1:def 3;
A107: n1 in Seg (len p1) by A106, FINSEQ_1:def 3;
reconsider n1 = n1 as Element of NAT by A106;
consider n2 being object such that
A108: ( n2 in dom p20 & y2 = p20 . n2 ) by A105, FUNCT_1:def 3;
A109: n2 in Seg (len p20) by A108, FINSEQ_1:def 3;
reconsider n2 = n2 as Element of NAT by A108;
A110: y2 = p2 . n2 by A108, FUNCT_1:47;
A111: ( 1 <= n1 & n1 <= len p1 ) by A107, FINSEQ_1:1;
A112: ( 1 <= n2 & n2 <= len p20 ) by A109, FINSEQ_1:1;
reconsider n11 = n1 - 1 as Element of NAT by A111, INT_1:5;
reconsider n21 = n2 - 1 as Element of NAT by A112, INT_1:5;
set k1 = n11 + ((len p1) * n21);
A113: n11 <= (len p1) - 1 by A111, XREAL_1:9;
(len p1) - 1 < len p1 by XREAL_1:44;
then A114: n11 < len p1 by A113, XXREAL_0:2;
A115: (n11 + ((len p1) * n21)) div (len p1) = (n11 div (len p1)) + n21 by A62, NAT_D:61
.= 0 + n21 by A114, NAT_D:27
.= n21 ;
A116: (n11 + ((len p1) * n21)) mod (len p1) = n11 mod (len p1) by NAT_D:61
.= n11 by A114, NAT_D:24 ;
set k = (n11 + ((len p1) * n21)) + 1;
A117: 1 <= (n11 + ((len p1) * n21)) + 1 by NAT_1:14;
A118: ((n11 + ((len p1) * n21)) + 1) -' 1 = ((n11 + ((len p1) * n21)) + 1) - 1 by NAT_1:14, XREAL_1:233
.= n11 + ((len p1) * n21) ;
then A119: n1 = ((((n11 + ((len p1) * n21)) + 1) -' 1) mod (len p1)) + 1 by A116;
A120: n2 = ((((n11 + ((len p1) * n21)) + 1) -' 1) div (len p1)) + 1 by A118, A115;
A121: (n11 + 1) + ((len p1) * n21) <= (len p1) + ((len p1) * n21) by A111, XREAL_1:6;
n21 <= (len p20) - 1 by A112, XREAL_1:9;
then (len p1) * n21 <= (len p1) * ((len p20) - 1) by XREAL_1:64;
then (len p1) + ((len p1) * n21) <= (len p1) + ((len p1) * ((len p20) - 1)) by XREAL_1:6;
then (n11 + ((len p1) * n21)) + 1 <= (len p1) * n by A121, A100, XXREAL_0:2;
then (n11 + ((len p1) * n21)) + 1 in Seg (len q30) by A117, A98;
then A122: (n11 + ((len p1) * n21)) + 1 in dom q30 by FINSEQ_1:def 3;
then A123: (n11 + ((len p1) * n21)) + 1 in dom q3 by RELAT_1:57;
q30 . ((n11 + ((len p1) * n21)) + 1) = q3 . ((n11 + ((len p1) * n21)) + 1) by A122, FUNCT_1:47
.= z by A105, A106, A110, A50, A123, A119, A120 ;
hence z in rng q30 by A122, FUNCT_1:3; :: thesis:

end;

then A124: [:Y1,Y20:] c= rng q30 ;

now :: thesis:

end;

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

end;

now :: thesis:

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

end;

then A138: Sum (Func_Seq (G,q30)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p20))) by A46, A102, A103, A104, A100;
dom F1 = DX1 by FUNCT_2:def 1;
then A139: dom (F1 * p1) = dom p1 by A1, RELAT_1:27
.= Seg (len p1) by FINSEQ_1:def 3 ;
A140: dom G = [:DX1,DX2:] by FUNCT_2:def 1;
len q3 = (n * (len p1)) + (len p1) by A48, A49;
then A141: n * (len p1) <= len q3 by NAT_1:11;
then A142: len q31 = (len q3) - ((len p1) * n) by RFINSEQ:def 1
.= len p1 by A48, A49 ;
A143: ( [:Y1,Y2:] c= [:DX1,DX2:] & rng q31 c= rng q3 ) by A48, FINSEQ_5:33;
then A144: dom (G * q31) = dom q31 by A140, RELAT_1:27
.= Seg (len p1) by A142, FINSEQ_1:def 3 ;
then A145: dom (G * q31) = dom (((Func_Seq (F2,p2)) /. (n + 1)) (#) (F1 * p1)) by A139, VALUED_1:def 5;

now :: thesis:

let x be object ; :: thesis:
assume A146: x in dom (G * q31) ; :: thesis:
then reconsider nx = x as Element of NAT ;
A147: dom (G * q31) = dom q31 by A140, A143, RELAT_1:27
.= Seg (len q31) by FINSEQ_1:def 3 ;
A148: ( 1 <= nx & nx <= len p1 ) by A146, A144, FINSEQ_1:1;
then A149: p1 /. nx = p1 . nx by FINSEQ_4:15;
A150: ( 1 <= n + 1 & n + 1 <= len p2 ) by A48, XREAL_1:31;
then A151: n + 1 in Seg (len p2) ;
then A152: n + 1 in dom p2 by FINSEQ_1:def 3;
A153: p2 /. (n + 1) = p2 . (n + 1) by A150, FINSEQ_4:15;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2 ;
then A154: n + 1 in dom (F2 * p2) by A152, RELAT_1:27;
A155: F2 . (p2 /. (n + 1)) = (F2 * p2) . (n + 1) by A152, A153, FUNCT_1:13
.= (Func_Seq (F2,p2)) /. (n + 1) by A154, PARTFUN1:def 6 ;
A156: ( 1 <= nx & nx <= len p1 ) by A147, A146, A142, FINSEQ_1:1;
then A157: nx + ((len p1) * n) <= (len p1) + ((len p1) * n) by XREAL_1:6;
A158: nx <= nx + ((len p1) * n) by NAT_1:11;
then ( 1 <= nx + ((len p1) * n) & nx + ((len p1) * n) <= (len p1) * (len p2) ) by A157, A48, A156, XXREAL_0:2;
then nx + ((len p1) * n) in dom FG by A51;
then A159: 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 A50;
A160: nx in dom q31 by A147, A146, FINSEQ_1:def 3;
A161: (nx + ((len p1) * n)) -' 1 = (nx + ((len p1) * n)) - 1 by A158, A156, XREAL_1:233, XXREAL_0:2
.= (nx - 1) + ((len p1) * n)
.= (nx -' 1) + ((len p1) * n) by A148, XREAL_1:233 ;
nx - 1 < nx by XREAL_1:44;
then nx - 1 < len p1 by A156, XXREAL_0:2;
then A162: nx -' 1 < len p1 by A148, XREAL_1:233;
A163: (((nx -' 1) + ((len p1) * n)) div (len p1)) + 1 = (((nx -' 1) div (len p1)) + n) + 1 by A62, NAT_D:61
.= (0 + n) + 1 by A162, NAT_D:27 ;
A164: (((nx -' 1) + ((len p1) * n)) mod (len p1)) + 1 = ((nx -' 1) mod (len p1)) + 1 by NAT_D:61
.= (nx -' 1) + 1 by A162, NAT_D:24
.= (nx - 1) + 1 by A148, XREAL_1:233 ;
A165: ( nx in dom p1 & n + 1 in dom p2 ) by A146, A144, A151, FINSEQ_1:def 3;
then ( p1 /. nx = p1 . nx & p2 . (n + 1) = p2 /. (n + 1) ) by PARTFUN1:def 6;
then A166: q31 . nx = [(p1 /. nx),(p2 /. (n + 1))] by A160, A159, A141, A161, A163, A164, RFINSEQ:def 1;
( p1 . nx in Y1 & p2 . (n + 1) in Y2 ) by A165, A48, A1, FUNCT_1:3;
then A167: ( p1 /. nx in Y1 & p2 /. (n + 1) in Y2 ) by A165, PARTFUN1:def 6;
thus (G * q31) . x = G . ((p1 /. nx),(p2 /. (n + 1))) by A166, A146, FUNCT_1:12
.= (F1 . (p1 /. nx)) * (F2 . (p2 /. (n + 1))) by A48, A167
.= ((F1 * p1) . nx) * ((Func_Seq (F2,p2)) /. (n + 1)) by A155, A149, A139, A146, A144, FUNCT_1:12
.= (((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 A145, FUNCT_1:2;
then A168: Sum (Func_Seq (G,q31)) = (Sum (Func_Seq (F1,p1))) * ((Func_Seq (F2,p2)) /. (n + 1)) by RVSUM_1:87;
A169: Func_Seq (G,q3) = (Func_Seq (G,q30)) ^ (Func_Seq (G,q31)) by A99, Lm5;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2 ;
then dom (F2 * p2) = dom p2 by RELAT_1:27;
then dom (Func_Seq (F2,p2)) = Seg (len p2) by FINSEQ_1:def 3;
then A170: len (Func_Seq (F2,p2)) = n + 1 by A48, FINSEQ_1:def 3;
(Func_Seq (F2,p2)) | n = Func_Seq (F2,p20) by RELAT_1:83;
then A171: Func_Seq (F2,p2) = (Func_Seq (F2,p20)) ^ <*((Func_Seq (F2,p2)) /. (n + 1))*> by A170, FINSEQ_5:21;
A172: Sum (Func_Seq (G,q3)) = (Sum (Func_Seq (G,q30))) + (Sum (Func_Seq (G,q31))) by A169, RVSUM_1:75
.= (Sum (Func_Seq (F1,p1))) * ((Sum (Func_Seq (F2,p20))) + ((Func_Seq (F2,p2)) /. (n + 1))) by A138, A168
.= (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A171, RVSUM_1:74 ;
consider P being Permutation of (dom p3) such that
A173: ( q3 = p3 * P & dom P = dom p3 & rng P = dom p3 ) by A75, A76, A48, BHSP_5:1;
A174: Func_Seq (G,q3) = (Func_Seq (G,p3)) * P by A173, RELAT_1:36;
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:27;
hence Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2))) by A172, A174, FINSOP_1:7; :: thesis:

end;

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

end;

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

end;

A175: for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A45);

now :: thesis:

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: