let n be non zero Nat; :: thesis:
let Xn be non-empty n -element FinSequence; :: thesis:
let X1 be non-empty 1 -element FinSequence; :: thesis:
let Sn be SemiringFamily of Xn; :: thesis:
let S1 be SemiringFamily of X1; :: thesis:
assume that
A1: SemiringProduct Sn is semiring_of_sets of (product Xn) and
A2: SemiringProduct S1 is semiring_of_sets of (product X1) ; :: thesis:
let S12 be Subset-Family of [:(product Xn),(product X1):]; :: thesis:
assume A2b: S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } ; :: thesis:
reconsider S12 = S12 as semiring_of_sets of [:(product Xn),(product X1):] by A1, A2, A2b, Thm29;
A3: ( 1 in Seg 1 & S1 is SemiringFamily of X1 ) by FINSEQ_1:3;
then A4: S1 . 1 is semiring_of_sets of (X1 . 1) by Def2;
A5: not S1 . 1 is empty by A3, Def2;
A6: 1 in Seg 1 by FINSEQ_1:3;
then A7: union (S1 . 1) c= X1 . 1 by Thm17;
consider I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) such that
A8: I is one-to-one and
A9: I is onto and
A10: for x, y being FinSequence st x in product Xn & y in product X1 holds
I . (x,y) = x ^ y by PRVECT_3:6;
take I ; :: thesis:
I .: S12 = SemiringProduct (Sn ^ S1)

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let t be object ; :: thesis:
assume t in I .: S12 ; :: thesis:
then consider s12 being Subset of [:(product Xn),(product X1):] such that
A12: s12 in S12 and
A13: t = I .: s12 by FUNCT_2:def 10;
consider s1 being Element of SemiringProduct Sn, s2 being Element of SemiringProduct S1 such that
A14: s12 = [:s1,s2:] by A2b, A12;
consider g1 being Function such that
A15: s1 = product g1 and
A16: g1 in product Sn by A1, Def3;
A17: s2 in SemiringProduct S1 by A2;
s2 in { (product <*s*>) where s is Element of S1 . 1 : verum } by A17, Thm24;
then consider s11 being Element of S1 . 1 such that
A18: s2 = product <*s11*> ;
reconsider g1 = g1 as n -element FinSequence by A16, Thm18;
A19: ( dom Xn = Seg n & dom Sn = Seg n & dom X1 = Seg 1 & dom S1 = Seg 1 ) by FINSEQ_1:89;
A20: dom g1 = Seg n by FINSEQ_1:89;
A21: len g1 = n by FINSEQ_3:153;
A22: dom (g1 ^ <*s11*>) = Seg (n + 1) by FINSEQ_1:89;
A23: dom I = [:(product Xn),(product X1):] by FUNCT_2:def 1;

now :: thesis:

product (g1 ^ <*s11*>) = I .: [:(product g1),(product <*s11*>):]

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let u be object ; :: thesis:
assume u in product (g1 ^ <*s11*>) ; :: thesis:
then consider v being Function such that
A24: u = v and
A25: dom v = dom (g1 ^ <*s11*>) and
A26: for y being object st y in dom (g1 ^ <*s11*>) holds
v . y in (g1 ^ <*s11*>) . y by CARD_3:def 5;
A27: dom v = Seg (n + 1) by A25, FINSEQ_1:89;
then reconsider v = v as FinSequence by FINSEQ_1:def 2;
card (dom v) = card (Seg (n + 1)) by A25, FINSEQ_1:89;
then card (dom v) = n + 1 by FINSEQ_1:57;
then card v = n + 1 by CARD_1:62;
then reconsider v = v as n + 1 -element FinSequence by CARD_1:def 7;
reconsider v1 = v | (Seg n) as FinSequence by FINSEQ_1:15;
len v = n + 1 by FINSEQ_3:153;
then A28: n <= len v by NAT_1:11;
then A29: dom v1 = Seg n by FINSEQ_1:17;
set w = [(v | (Seg n)),<*(v . (n + 1))*>];

A30: now :: thesis:

now :: thesis:

A31: ( dom (v | (Seg n)) = Seg n & dom Xn = Seg n ) by A29, FINSEQ_1:89;
thus dom (v | (Seg n)) = dom Xn by A29, FINSEQ_1:89; :: thesis:
let y be object ; :: thesis:
assume A32: y in dom Xn ; :: thesis:
then A33: ( y in Seg n & Seg n c= Seg (n + 1) ) by FINSEQ_1:89, FINSEQ_3:18;
y in dom (v | (Seg n)) by A32, FINSEQ_1:89, A29;
then A34: (v | (Seg n)) . y = v . y by FUNCT_1:47;
A35: v . y in (g1 ^ <*s11*>) . y by A33, A22, A26;
A36: (v | (Seg n)) . y in g1 . y by A34, A35, A32, A20, A31, FINSEQ_1:def 7;
A37: ( g1 in product Sn & y in dom Sn ) by A16, A32, Thm16;
consider gg being Function such that
A38: gg = g1 and
dom gg = dom Sn and
A39: for y being object st y in dom Sn holds
gg . y in Sn . y by A16, CARD_3:def 5;
g1 . y in Sn . y by A37, A38, A39;
then A40: ( (v | (Seg n)) . y in union (Sn . y) & y in Seg n ) by A32, FINSEQ_1:89, A36, TARSKI:def 4;
union (Sn . y) c= Xn . y by A33, Thm17;
hence (v | (Seg n)) . y in Xn . y by A40; :: thesis:

end;

hence v | (Seg n) in product Xn by CARD_3:def 5; :: thesis:
A41: v . (n + 1) in (g1 ^ <*s11*>) . (n + 1) by A22, FINSEQ_1:4, A26;
(g1 ^ <*s11*>) . (n + 1) = s11 by A21, FINSEQ_1:42;
then ( v . (n + 1) in union (S1 . 1) & union (S1 . 1) c= X1 . 1 ) by A41, A5, A6, Thm17, TARSKI:def 4;
then <*(v . (n + 1))*> in { <*a*> where a is Element of X1 . 1 : verum } ;
hence <*(v . (n + 1))*> in product X1 by Thm21; :: thesis:

end;

now :: thesis:

thus [(v | (Seg n)),<*(v . (n + 1))*>] in dom I by ZFMISC_1:def 2, A30, A23; :: thesis:

now :: thesis:

thus dom v1 = dom g1 by A28, FINSEQ_1:17, A20; :: thesis:

now :: thesis:

let y be object ; :: thesis:
assume A42: y in dom g1 ; :: thesis:
then A43: ( y in Seg n & Seg n c= Seg (n + 1) ) by FINSEQ_1:89, FINSEQ_3:18;
A44: (v | (Seg n)) . y = v . y by A42, A20, A29, FUNCT_1:47;
v . y in (g1 ^ <*s11*>) . y by A43, A22, A26;
hence v1 . y in g1 . y by A44, A42, FINSEQ_1:def 7; :: thesis:

end;

hence for y being object st y in dom g1 holds
v1 . y in g1 . y ; :: thesis:

end;

hence v | (Seg n) in product g1 by CARD_3:def 5; :: thesis:
A46: v . (n + 1) in (g1 ^ <*s11*>) . (n + 1) by A22, A26, FINSEQ_1:4;

now :: thesis:

( dom <*(v . (n + 1))*> = Seg 1 & dom <*s11*> = Seg 1 ) by FINSEQ_1:def 8;
hence dom <*(v . (n + 1))*> = dom <*s11*> ; :: thesis:
let y be object ; :: thesis:
assume y in dom <*s11*> ; :: thesis:
then ( y in Seg 1 & Seg 1 = {1} ) by FINSEQ_1:def 8, FINSEQ_1:2;
then A47: y = 1 by TARSKI:def 1;
( <*(v . (n + 1))*> . 1 = v . (n + 1) & <*s11*> . 1 = s11 ) by FINSEQ_1:def 8;
hence <*(v . (n + 1))*> . y in <*s11*> . y by A21, A46, FINSEQ_1:42, A47; :: thesis:

end;

hence <*(v . (n + 1))*> in product <*s11*> by CARD_3:def 5; :: thesis:

end;

hence [(v | (Seg n)),<*(v . (n + 1))*>] in [:(product g1),(product <*s11*>):] by ZFMISC_1:def 2; :: thesis:
A48: I . [(v | (Seg n)),<*(v . (n + 1))*>] = I . (v1,<*(v . (n + 1))*>) by BINOP_1:def 1;
v1 ^ <*(v . (n + 1))*> = v | (Seg (n + 1)) by A27, FINSEQ_1:4, FINSEQ_5:10;
hence u = I . [(v | (Seg n)),<*(v . (n + 1))*>] by A48, A30, A10, A24, A27; :: thesis:

end;

hence u in I .: [:(product g1),(product <*s11*>):] by FUNCT_1:def 6; :: thesis:

end;

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in I .: [:(product g1),(product <*s11*>):] ; :: thesis:
then consider v being object such that
v in dom I and
A50: v in [:(product g1),(product <*s11*>):] and
A51: u = I . v by FUNCT_1:def 6;
consider va, vb being object such that
A52: va in product g1 and
A53: vb in product <*s11*> and
A54: v = [va,vb] by A50, ZFMISC_1:def 2;
consider wa being Function such that
A55: wa = va and
A56: dom wa = dom g1 and
A57: for y being object st y in dom g1 holds
wa . y in g1 . y by A52, CARD_3:def 5;
consider wb being Function such that
A58: wb = vb and
A59: dom wb = dom <*s11*> and
A60: for y being object st y in dom <*s11*> holds
wb . y in <*s11*> . y by A53, CARD_3:def 5;
A61: dom g1 = Seg n by FINSEQ_1:89;
then reconsider wa = wa as FinSequence by A56, FINSEQ_1:def 2;
reconsider wa = wa as n -element FinSequence by A55, A52, Thm18;
reconsider wb = wb as FinSequence by A59, FINSEQ_1:def 8, FINSEQ_1:def 2;
card (dom wb) = 1 by A59, CARD_1:def 7;
then card wb = 1 by CARD_1:62;
then reconsider wb = wb as 1 -element FinSequence by CARD_1:def 7;
reconsider w = wa ^ wb as n + 1 -element FinSequence ;

now :: thesis:

A62: now :: thesis:

now :: thesis:

thus dom wa = dom Xn by FINSEQ_1:89, A19; :: thesis:
let y be object ; :: thesis:
assume A63: y in dom Xn ; :: thesis:
then y in dom g1 by FINSEQ_1:89, A19;
then A64: wa . y in g1 . y by A57;
consider gg1 being Function such that
A65: gg1 = g1 and
dom gg1 = dom Sn and
A66: for y being object st y in dom Sn holds
gg1 . y in Sn . y by A16, CARD_3:def 5;
g1 . y in Sn . y by A63, A19, A65, A66;
then A67: wa . y in union (Sn . y) by A64, TARSKI:def 4;
union (Sn . y) c= Xn . y by A63, A19, Thm17;
hence wa . y in Xn . y by A67; :: thesis:

end;

hence wa in product Xn by CARD_3:def 5; :: thesis:

now :: thesis:

thus dom wb = dom X1 by FINSEQ_1:89, A19; :: thesis:
let y be object ; :: thesis:
assume A68: y in dom X1 ; :: thesis:
y in dom <*s11*> by A68, A19, FINSEQ_1:def 8;
then A69: wb . y in <*s11*> . y by A60;
A70: y = 1 by A68, A19, FINSEQ_1:2, TARSKI:def 1;
then A71: wb . y in s11 by A69, FINSEQ_1:def 8;
wb . y in union (S1 . 1) by A71, A5, TARSKI:def 4;
hence wb . y in X1 . y by A70, A7; :: thesis:

end;

hence wb in product X1 by CARD_3:def 5; :: thesis:

end;

I . [va,vb] = I . (wa,wb) by A55, A58, BINOP_1:def 1;
hence u = w by A54, A51, A10, A62; :: thesis:
A73: ( dom (g1 ^ <*s11*>) = Seg (n + 1) & dom w = Seg (n + 1) ) by FINSEQ_1:89;
hence dom w = dom (g1 ^ <*s11*>) ; :: thesis:

hereby :: thesis:

let y be object ; :: thesis:
assume y in dom (g1 ^ <*s11*>) ; :: thesis:
then y in (Seg n) \/ {(n + 1)} by A73, FINSEQ_1:9;
then ( y in Seg n or y in {(n + 1)} ) by XBOOLE_0:def 3;

per cases by TARSKI:def 1;

suppose A74: y in Seg n ; :: thesis:

then A75: y in dom g1 by FINSEQ_1:89;
( (g1 ^ <*s11*>) . y = g1 . y & wa . y in g1 . y ) by A74, A61, A57, FINSEQ_1:def 7;
hence w . y in (g1 ^ <*s11*>) . y by A56, FINSEQ_1:def 7, A75; :: thesis:

end;

suppose A77: y = n + 1 ; :: thesis:

then A78: (g1 ^ <*s11*>) . y = s11 by A21, FINSEQ_1:42;
dom wb = dom X1 by FINSEQ_1:89, A19;
then 1 in dom wb by A19, FINSEQ_1:2, TARSKI:def 1;
then A79: wb . 1 = w . ((len wa) + 1) by FINSEQ_1:def 7;
A80: (len wa) + 1 = n + 1 by FINSEQ_3:153;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*s11*> by FINSEQ_1:def 8;
then w . y in <*s11*> . 1 by A60, A80, A77, A79;
hence w . y in (g1 ^ <*s11*>) . y by A78, FINSEQ_1:def 8; :: thesis:

end;

hence u in product (g1 ^ <*s11*>) by CARD_3:def 5; :: thesis:

end;

hence t = product (g1 ^ <*s11*>) by A13, A14, A15, A18; :: thesis:

now :: thesis:

A81: len (Sn ^ S1) = n + 1 by FINSEQ_3:153;
then A82: dom (Sn ^ S1) = Seg (n + 1) by FINSEQ_1:def 3;
thus dom (g1 ^ <*s11*>) = dom (Sn ^ S1) by A81, A22, FINSEQ_1:def 3; :: thesis:
let u be object ; :: thesis:
assume u in dom (Sn ^ S1) ; :: thesis:
then u in (Seg n) \/ {(n + 1)} by A82, FINSEQ_1:9;
then ( u in Seg n or u in {(n + 1)} ) by XBOOLE_0:def 3;

per cases by TARSKI:def 1;

suppose A83: u in Seg n ; :: thesis:

then A84: u in dom Sn by FINSEQ_1:89;
A85: (Sn ^ S1) . u = Sn . u by A19, A83, FINSEQ_1:def 7;
dom g1 = Seg n by FINSEQ_1:89;
then A86: (g1 ^ <*s11*>) . u = g1 . u by A83, FINSEQ_1:def 7;
consider gg1 being Function such that
A87: g1 = gg1 and
dom gg1 = dom Sn and
A88: for y being object st y in dom Sn holds
gg1 . y in Sn . y by A16, CARD_3:def 5;
thus (g1 ^ <*s11*>) . u in (Sn ^ S1) . u by A87, A88, A84, A86, A85; :: thesis:

end;

suppose A89: u = n + 1 ; :: thesis:

then A90: (g1 ^ <*s11*>) . u = s11 by A21, FINSEQ_1:42;
A91: s11 in S1 . 1 by A5;
( 1 in dom S1 & len Sn = n ) by A19, FINSEQ_1:3, FINSEQ_3:153;
hence (g1 ^ <*s11*>) . u in (Sn ^ S1) . u by A89, A90, A91, FINSEQ_1:def 7; :: thesis:

end;

hence g1 ^ <*s11*> in product (Sn ^ S1) by CARD_3:def 5; :: thesis:

end;

hence t in SemiringProduct (Sn ^ S1) by Def3; :: thesis:

end;

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in SemiringProduct (Sn ^ S1) ; :: thesis:
then consider f being Function such that
A92: t = product f and
A93: f in product (Sn ^ S1) by Def3;
consider g being Function such that
A94: f = g and
A95: dom g = dom (Sn ^ S1) and
A96: for y being object st y in dom (Sn ^ S1) holds
g . y in (Sn ^ S1) . y by A93, CARD_3:def 5;
A97: ( dom Xn = Seg n & dom Sn = Seg n & dom X1 = Seg 1 & dom S1 = Seg 1 ) by FINSEQ_1:89;
( dom X1 = {1} & dom S1 = {1} ) by FINSEQ_1:2, FINSEQ_1:89;
then A98: ( 1 in dom X1 & 1 in dom S1 ) by TARSKI:def 1;
A99: ( len Xn = n & len Sn = n & len X1 = 1 & len S1 = 1 ) by FINSEQ_3:153;
A100: len (Sn ^ S1) = n + 1 by FINSEQ_3:153;
then A101: dom (Sn ^ S1) = Seg (n + 1) by FINSEQ_1:def 3;
dom g = Seg (n + 1) by A95, A100, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
card (dom g) = n + 1 by A95, CARD_1:def 7;
then card g = n + 1 by CARD_1:62;
then reconsider g = g as n + 1 -element FinSequence by CARD_1:def 7;
reconsider t0 = t as set by TARSKI:1;

now :: thesis:

let a be object ; :: thesis:
assume a in product f ; :: thesis:
then consider b being Function such that
A102: a = b and
A103: dom b = dom f and
A104: for y being object st y in dom f holds
b . y in f . y by CARD_3:def 5;

now :: thesis:

take b = b; :: thesis:
thus a = b by A102; :: thesis:
len (Sn ^ S1) = n + 1 by FINSEQ_3:153;
then A105: dom (Sn ^ S1) = Seg (n + 1) by FINSEQ_1:def 3;
A106: dom f = Seg (n + 1) by A105, A93, CARD_3:9;
A107: dom b = Seg (n + 1) by A103, A105, A93, CARD_3:9;
A108: len (Xn ^ X1) = n + 1 by FINSEQ_3:153;
then A109: dom (Xn ^ X1) = Seg (n + 1) by FINSEQ_1:def 3;
thus dom b = dom (Xn ^ X1) by A108, A107, FINSEQ_1:def 3; :: thesis:
let y be object ; :: thesis:
assume A110: y in dom (Xn ^ X1) ; :: thesis:
then A111: b . y in f . y by A104, A106, A109;
g . y in (Sn ^ S1) . y by A96, A105, A109, A110;
then A112: b . y in union ((Sn ^ S1) . y) by A111, A94, TARSKI:def 4;
y in (Seg n) \/ {(n + 1)} by A110, A109, FINSEQ_1:9;
then ( y in Seg n or y in {(n + 1)} ) by XBOOLE_0:def 3;

per cases by TARSKI:def 1;

suppose A113: y in Seg n ; :: thesis:

then A114: (Xn ^ X1) . y = Xn . y by A97, FINSEQ_1:def 7;
Sn . y is semiring_of_sets of (Xn . y) by A113, Def2;
then union (Sn . y) c= union (bool (Xn . y)) by ZFMISC_1:77;
then ( union (Sn . y) c= Xn . y & union ((Sn ^ S1) . y) = union (Sn . y) ) by ZFMISC_1:81, A97, A113, FINSEQ_1:def 7;
hence b . y in (Xn ^ X1) . y by A112, A114; :: thesis:

end;

suppose A116: y = n + 1 ; :: thesis:

then A117: (Xn ^ X1) . y = X1 . 1 by A99, A98, FINSEQ_1:def 7;
union (S1 . 1) c= union (bool (X1 . 1)) by A4, ZFMISC_1:77;
then ( union (S1 . 1) c= X1 . 1 & union ((Sn ^ S1) . y) = union (S1 . 1) ) by A116, A99, A98, FINSEQ_1:def 7, ZFMISC_1:81;
hence b . y in (Xn ^ X1) . y by A112, A117; :: thesis:

end;

hence a in product (Xn ^ X1) by CARD_3:def 5; :: thesis:

end;

then t0 c= product (Xn ^ X1) by A92;
then reconsider t1 = t0 as Subset of (product (Xn ^ X1)) ;
reconsider hn = product (g | n) as set ;
( n <= n + 1 & len g = n + 1 ) by NAT_1:11, FINSEQ_3:153;
then A118b: len (g | n) = n by FINSEQ_1:59;
then A119: dom (g | n) = Seg n by FINSEQ_1:def 3;

A120: now :: thesis:

let a be object ; :: thesis:
assume a in hn ; :: thesis:
then consider b being Function such that
A121: a = b and
A122: dom b = dom (g | n) and
A123: for y being object st y in dom (g | n) holds
b . y in (g | n) . y by CARD_3:def 5;

now :: thesis:

thus dom b = dom Xn by A122, A118b, FINSEQ_1:def 3, A97; :: thesis:
let y be object ; :: thesis:
assume A124: y in dom Xn ; :: thesis:
then A125: y in Seg n by FINSEQ_1:89;
b . y in (g | n) . y by A124, A97, A119, A123;
then b . y in (g | (Seg n)) . y by FINSEQ_1:def 15;
then A126: b . y in g . y by A125, FUNCT_1:49;
Seg n c= Seg (n + 1) by NAT_1:11, FINSEQ_1:5;
then A127: g . y in (Sn ^ S1) . y by A101, A96, A125;
g . y in Sn . y by A124, A127, A97, FINSEQ_1:def 7;
then A128: b . y in union (Sn . y) by A126, TARSKI:def 4;
Sn . y is semiring_of_sets of (Xn . y) by A125, Def2;
then union (Sn . y) c= union (bool (Xn . y)) by ZFMISC_1:77;
then union (Sn . y) c= Xn . y by ZFMISC_1:81;
hence b . y in Xn . y by A128; :: thesis:

end;

hence a in product Xn by A121, CARD_3:def 5; :: thesis:

end;

then A129: hn c= product Xn ;
reconsider h1 = product <*(g . (n + 1))*> as set ;

A130: now :: thesis:

let a be object ; :: thesis:
assume a in h1 ; :: thesis:
then consider b being Function such that
A131: a = b and
A132: dom b = dom <*(g . (n + 1))*> and
A133: for y being object st y in dom <*(g . (n + 1))*> holds
b . y in <*(g . (n + 1))*> . y by CARD_3:def 5;
A134: dom <*(g . (n + 1))*> = Seg 1 by FINSEQ_1:def 8;

now :: thesis:

thus dom b = dom X1 by A132, FINSEQ_1:def 8, A97; :: thesis:
let y be object ; :: thesis:
assume A135: y in dom X1 ; :: thesis:
then A136: y in Seg 1 by FINSEQ_1:89;
A137: b . y in <*(g . (n + 1))*> . y by A135, A133, A134, A97;
A138: y = 1 by A136, FINSEQ_1:2, TARSKI:def 1;
( 1 in dom S1 & len Sn = n ) by A97, FINSEQ_1:3, FINSEQ_3:153;
then ( (Sn ^ S1) . ((len Sn) + 1) = S1 . 1 & dom (Sn ^ S1) = Seg (n + 1) ) by A99, FINSEQ_1:def 7;
then ( b . y in g . (n + 1) & g . (n + 1) in S1 . 1 ) by A138, A137, FINSEQ_1:def 8, A96, A99, FINSEQ_1:3;
then A139: b . y in union (S1 . 1) by TARSKI:def 4;
union (S1 . 1) c= union (bool (X1 . 1)) by A4, ZFMISC_1:77;
then union (S1 . 1) c= X1 . 1 by ZFMISC_1:81;
hence b . y in X1 . y by A139, A138; :: thesis:

end;

hence a in product X1 by A131, CARD_3:def 5; :: thesis:

end;

then h1 c= product X1 ;
then reconsider s12 = [:hn,h1:] as Subset of [:(product Xn),(product X1):] by A129, ZFMISC_1:96;

now :: thesis:

thus hn = product (g | n) ; :: thesis:

now :: thesis:

thus dom (g | n) = dom Sn by A119, FINSEQ_1:89; :: thesis:
let y be object ; :: thesis:
assume A140: y in dom Sn ; :: thesis:
then A141: y in Seg n by FINSEQ_1:89;
Seg n c= Seg (n + 1) by NAT_1:11, FINSEQ_1:5;
then A142: g . y in (Sn ^ S1) . y by A96, A101, A141;
A143: g . y in Sn . y by A142, A140, FINSEQ_1:def 7;
y in dom (g | (Seg n)) by A141, A119, FINSEQ_1:def 15;
then g . y = (g | (Seg n)) . y by FUNCT_1:47;
hence (g | n) . y in Sn . y by A143, FINSEQ_1:def 15; :: thesis:

end;

hence g | n in product Sn by CARD_3:def 5; :: thesis:

end;

hence hn is Element of SemiringProduct Sn by Def3; :: thesis:

now :: thesis:

thus h1 = product <*(g . (n + 1))*> ; :: thesis:

now :: thesis:

thus dom <*(g . (n + 1))*> = dom S1 by FINSEQ_1:def 8, A97; :: thesis:
let b be object ; :: thesis:
assume b in dom S1 ; :: thesis:
then A144: b = 1 by A97, FINSEQ_1:2, TARSKI:def 1;
A145: <*(g . (n + 1))*> . 1 = g . (n + 1) by FINSEQ_1:def 8;
( <*(g . (n + 1))*> . 1 in (Sn ^ S1) . (n + 1) & 1 in dom S1 ) by A96, FINSEQ_1:4, A101, A145, A97, FINSEQ_1:2, TARSKI:def 1;
hence <*(g . (n + 1))*> . b in S1 . b by A144, A99, FINSEQ_1:def 7; :: thesis:

end;

hence <*(g . (n + 1))*> in product S1 by CARD_3:def 5; :: thesis:

end;

hence h1 is Element of SemiringProduct S1 by Def3; :: thesis:

end;

hence s12 in S12 by A2b; :: thesis:

now :: thesis:

hereby :: thesis:

let u be object ; :: thesis:
assume u in I .: [:hn,h1:] ; :: thesis:
then consider v being object such that
v in dom I and
A146: v in [:hn,h1:] and
A147: u = I . v by FUNCT_1:def 6;
consider va, vb being object such that
A148: va in hn and
A149: vb in h1 and
A150: v = [va,vb] by A146, ZFMISC_1:def 2;
A151: ( va in product Xn & vb in product X1 ) by A120, A130, A148, A149;
reconsider va = va as n -element FinSequence by A120, A148, Thm18;
reconsider vb = vb as 1 -element FinSequence by A149, Thm18;
A152: u = I . (va,vb) by A147, A150, BINOP_1:def 1
.= va ^ vb by A10, A151 ;
set vab = va ^ vb;
len (Sn ^ S1) = n + 1 by FINSEQ_3:153;
then A153: dom (Sn ^ S1) = Seg (n + 1) by FINSEQ_1:def 3;
then A154: dom f = Seg (n + 1) by A93, CARD_3:9;
A155: dom (va ^ vb) = Seg (n + 1) by FINSEQ_1:89;

now :: thesis:

thus dom (va ^ vb) = dom f by A153, A93, CARD_3:9, A155; :: thesis:
let y be object ; :: thesis:
assume y in dom f ; :: thesis:
then y in (Seg n) \/ {(n + 1)} by A154, FINSEQ_1:9;
then ( y in Seg n or y in {(n + 1)} ) by XBOOLE_0:def 3;

per cases by TARSKI:def 1;

suppose A156: y in Seg n ; :: thesis:

then A157: y in dom va by FINSEQ_1:89;
then A158: (va ^ vb) . y = va . y by FINSEQ_1:def 7;
consider va1 being Function such that
A159: va1 = va and
A160: dom va1 = dom (g | n) and
A161: for y being object st y in dom (g | n) holds
va1 . y in (g | n) . y by A148, CARD_3:def 5;
va1 . y in (g | n) . y by A157, A159, A160, A161;
then va1 . y in (g | (Seg n)) . y by FINSEQ_1:def 15;
hence (va ^ vb) . y in f . y by A94, A156, A158, A159, FUNCT_1:49; :: thesis:

end;

suppose A162: y = n + 1 ; :: thesis:

now :: thesis:

dom vb = Seg 1 by FINSEQ_1:89;
hence 1 in dom vb by FINSEQ_1:2, TARSKI:def 1; :: thesis:
thus y = (len va) + 1 by A162, FINSEQ_3:153; :: thesis:

end;

then A163: (va ^ vb) . y = vb . 1 by FINSEQ_1:def 7;
consider vb1 being Function such that
A164: vb = vb1 and
dom vb1 = dom <*(g . (n + 1))*> and
A165: for y being object st y in dom <*(g . (n + 1))*> holds
vb1 . y in <*(g . (n + 1))*> . y by A149, CARD_3:def 5;
dom <*(g . (n + 1))*> = Seg 1 by FINSEQ_1:def 8;
then 1 in dom <*(g . (n + 1))*> by FINSEQ_1:2, TARSKI:def 1;
then vb1 . 1 in <*(g . (n + 1))*> . 1 by A165;
hence (va ^ vb) . y in f . y by A164, A163, A162, A94, FINSEQ_1:def 8; :: thesis:

end;

hence u in product f by A152, CARD_3:def 5; :: thesis:

end;

let u be object ; :: thesis:
assume u in product f ; :: thesis:
then consider v being Function such that
A166: u = v and
A167: dom v = dom f and
A168: for y being object st y in dom f holds
v . y in f . y by CARD_3:def 5;
len (Sn ^ S1) = n + 1 by FINSEQ_3:153;
then A169: dom (Sn ^ S1) = Seg (n + 1) by FINSEQ_1:def 3;
A170: dom f = Seg (n + 1) by A93, A169, CARD_3:9;
A171: dom v = Seg (n + 1) by A93, A167, A169, CARD_3:9;
reconsider v = v as FinSequence by A93, A167, A169, CARD_3:9, FINSEQ_1:def 2;
card (dom v) = n + 1 by A171, FINSEQ_1:57;
then card v = n + 1 by CARD_1:62;
then reconsider v = v as n + 1 -element FinSequence by CARD_1:def 7;
reconsider xn = v | (Seg n) as FinSequence by FINSEQ_1:15;
reconsider x1 = <*(v . (n + 1))*> as 1 -element FinSequence ;
A172: ( xn in product Xn & x1 in product X1 )

proof

now :: thesis:

len v = n + 1 by FINSEQ_3:153;
then A173: n <= len v by NAT_1:11;
then A174: dom xn = Seg n by FINSEQ_1:17;
thus dom xn = dom Xn by A173, FINSEQ_1:17, A97; :: thesis:
let y be object ; :: thesis:
assume A175: y in dom Xn ; :: thesis:
A176: ( y in Seg n & Seg n c= Seg (n + 1) ) by NAT_1:11, A175, FINSEQ_1:89, FINSEQ_1:5;
A177: v . y in f . y by A176, A170, A168;
A178: f . y in (Sn ^ S1) . y by A176, A101, A94, A96;
A179: f . y in Sn . y by A175, A97, A178, FINSEQ_1:def 7;
Sn . y is semiring_of_sets of (Xn . y) by A175, A97, Def2;
then union (Sn . y) c= union (bool (Xn . y)) by ZFMISC_1:77;
then A180: union (Sn . y) c= Xn . y by ZFMISC_1:81;
v . y in union (Sn . y) by A179, A177, TARSKI:def 4;
then v . y in Xn . y by A180;
hence xn . y in Xn . y by A174, A175, A97, FUNCT_1:47; :: thesis:

end;

hence xn in product Xn by CARD_3:def 5; :: thesis:

now :: thesis:

thus dom x1 = dom X1 by A97, FINSEQ_1:def 8; :: thesis:
let y be object ; :: thesis:
assume y in dom X1 ; :: thesis:
then A181: y = 1 by A97, FINSEQ_1:2, TARSKI:def 1;
then A182: x1 . y = v . (n + 1) by FINSEQ_1:def 8;
( 1 in dom S1 & len Sn = n ) by A97, FINSEQ_1:3, FINSEQ_3:153;
then ( (Sn ^ S1) . ((len Sn) + 1) = S1 . 1 & dom (Sn ^ S1) = Seg (n + 1) ) by A99, FINSEQ_1:def 7;
then ( v . (n + 1) in f . (n + 1) & f . (n + 1) in S1 . 1 ) by A99, A94, A96, A170, A168, FINSEQ_1:4;
then ( v . (n + 1) in union (S1 . 1) & union (S1 . 1) c= X1 . 1 ) by A6, Thm17, TARSKI:def 4;
hence x1 . y in X1 . y by A181, A182; :: thesis:

end;

hence x1 in product X1 by CARD_3:def 5; :: thesis:

end;

set x = [xn,x1];

now :: thesis:

dom I = [:(product Xn),(product X1):] by FUNCT_2:def 1;
hence [xn,x1] in dom I by A172, ZFMISC_1:def 2; :: thesis:

now :: thesis:

len v = n + 1 by FINSEQ_3:153;
then n <= len v by NAT_1:11;
then A183: dom xn = Seg n by FINSEQ_1:17;
then A184: ( dom (v | (Seg n)) = Seg n & Seg n = dom (g | n) ) by A118b, FINSEQ_1:def 3;
thus A185: dom (v | (Seg n)) = dom (g | n) by A183, A118b, FINSEQ_1:def 3; :: thesis:
let y be object ; :: thesis:
assume A186: y in dom (g | n) ; :: thesis:
then A187: (v | (Seg n)) . y = v . y by A185, FUNCT_1:47;
( Seg n c= Seg (n + 1) & dom (g | n) = Seg n & dom f = Seg (n + 1) ) by NAT_1:11, A118b, FINSEQ_1:def 3, A93, A169, CARD_3:9, FINSEQ_1:5;
then A188: v . y in g . y by A94, A168, A186;
(g | (Seg n)) . y = g . y by A186, A184, FUNCT_1:49;
hence (v | (Seg n)) . y in (g | n) . y by A187, A188, FINSEQ_1:def 15; :: thesis:

end;

hence xn in hn by CARD_3:def 5; :: thesis:

now :: thesis:

dom x1 = dom X1 by A97, FINSEQ_1:def 8;
hence dom x1 = dom <*(g . (n + 1))*> by A97, FINSEQ_1:def 8; :: thesis:
let y be object ; :: thesis:
assume y in dom <*(g . (n + 1))*> ; :: thesis:
then y in Seg 1 by FINSEQ_1:def 8;
then A189: y = 1 by FINSEQ_1:2, TARSKI:def 1;
then A190: <*(g . (n + 1))*> . y = g . (n + 1) by FINSEQ_1:def 8;
x1 . y = v . (n + 1) by A189, FINSEQ_1:def 8;
hence x1 . y in <*(g . (n + 1))*> . y by A168, A170, FINSEQ_1:4, A94, A190; :: thesis:

end;

hence x1 in h1 by CARD_3:def 5; :: thesis:
thus [xn,x1] = [xn,x1] ; :: thesis:

end;

hence [xn,x1] in [:hn,h1:] by ZFMISC_1:def 2; :: thesis:

now :: thesis:

A191: I . [xn,x1] = I . (xn,x1) by BINOP_1:def 1
.= xn ^ x1 by A10, A172 ;
xn ^ <*(v . (n + 1))*> = v | (Seg (n + 1)) by A171, FINSEQ_1:4, FINSEQ_5:10;
hence I . [xn,x1] = v by A171, A191; :: thesis:

end;

hence u = I . [xn,x1] by A166; :: thesis:

end;

hence u in I .: [:hn,h1:] by FUNCT_1:def 6; :: thesis:

end;

then ( I .: [:hn,h1:] c= product f & product f c= I .: [:hn,h1:] ) ;
hence t1 = I .: s12 by A92; :: thesis:

end;

hence t in I .: S12 by FUNCT_2:def 10; :: thesis:

end;

hence ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product Xn & y in product X1 holds
I . (x,y) = x ^ y ) & I .: S12 = SemiringProduct (Sn ^ S1) ) by A8, A9, A10; :: thesis: