let n be non zero Nat; for Xn being non-empty n -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being SemiringFamily of Xn
for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds
for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
let Xn be non-empty n -element FinSequence; for X1 being non-empty 1 -element FinSequence
for Sn being SemiringFamily of Xn
for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds
for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
let X1 be non-empty 1 -element FinSequence; for Sn being SemiringFamily of Xn
for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds
for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
let Sn be SemiringFamily of Xn; for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds
for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
let S1 be SemiringFamily of X1; ( SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) implies for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) ) )
assume that
A1:
SemiringProduct Sn is semiring_of_sets of (product Xn)
and
A2:
SemiringProduct S1 is semiring_of_sets of (product X1)
; for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
let S12 be Subset-Family of [:(product Xn),(product X1):]; ( S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } implies ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) ) )
assume A2b:
S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum }
; ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( 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) )
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
; ( 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) )
I .: S12 = SemiringProduct (Sn ^ S1)
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 SemiringProduct (Sn ^ S1) c= I .: S12
let t be
object ;
( t in I .: S12 implies t in SemiringProduct (Sn ^ S1) )assume
t in I .: S12
;
t in SemiringProduct (Sn ^ S1)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 ( t = product (g1 ^ <*s11*>) & g1 ^ <*s11*> in product (Sn ^ S1) )
product (g1 ^ <*s11*>) = I .: [:(product g1),(product <*s11*>):]
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 I .: [:(product g1),(product <*s11*>):] c= product (g1 ^ <*s11*>)
let u be
object ;
( u in product (g1 ^ <*s11*>) implies u in I .: [:(product g1),(product <*s11*>):] )assume
u in product (g1 ^ <*s11*>)
;
u in I .: [:(product g1),(product <*s11*>):]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 ( v | (Seg n) in product Xn & <*(v . (n + 1))*> in product X1 )now ( dom (v | (Seg n)) = dom Xn & ( for y being object st y in dom Xn holds
(v | (Seg n)) . y in Xn . y ) )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;
for y being object st y in dom Xn holds
(v | (Seg n)) . y in Xn . ylet y be
object ;
( y in dom Xn implies (v | (Seg n)) . y in Xn . y )assume A32:
y in dom Xn
;
(v | (Seg n)) . y in Xn . ythen 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;
verum end; hence
v | (Seg n) in product Xn
by CARD_3:def 5;
<*(v . (n + 1))*> in product X1A41:
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;
verum now ( [(v | (Seg n)),<*(v . (n + 1))*>] in dom I & [(v | (Seg n)),<*(v . (n + 1))*>] in [:(product g1),(product <*s11*>):] & u = I . [(v | (Seg n)),<*(v . (n + 1))*>] )thus
[(v | (Seg n)),<*(v . (n + 1))*>] in dom I
by ZFMISC_1:def 2, A30, A23;
( [(v | (Seg n)),<*(v . (n + 1))*>] in [:(product g1),(product <*s11*>):] & u = I . [(v | (Seg n)),<*(v . (n + 1))*>] )hence
[(v | (Seg n)),<*(v . (n + 1))*>] in [:(product g1),(product <*s11*>):]
by ZFMISC_1:def 2;
u = I . [(v | (Seg n)),<*(v . (n + 1))*>]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;
verum end; hence
u in I .: [:(product g1),(product <*s11*>):]
by FUNCT_1:def 6;
verum
end;
let u be
object ;
TARSKI:def 3 ( not u in I .: [:(product g1),(product <*s11*>):] or u in product (g1 ^ <*s11*>) )
assume
u in I .: [:(product g1),(product <*s11*>):]
;
u in product (g1 ^ <*s11*>)
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 ;
hence
u in product (g1 ^ <*s11*>)
by CARD_3:def 5;
verum
end; hence
t = product (g1 ^ <*s11*>)
by A13, A14, A15, A18;
g1 ^ <*s11*> in product (Sn ^ S1)hence
g1 ^ <*s11*> in product (Sn ^ S1)
by CARD_3:def 5;
verum end; hence
t in SemiringProduct (Sn ^ S1)
by Def3;
verum
end;
let t be
object ;
TARSKI:def 3 ( not t in SemiringProduct (Sn ^ S1) or t in I .: S12 )
assume
t in SemiringProduct (Sn ^ S1)
;
t in I .: S12
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 for a being object st a in product f holds
a in product (Xn ^ X1)let a be
object ;
( a in product f implies a in product (Xn ^ X1) )assume
a in product f
;
a in product (Xn ^ X1)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 ex b being Function st
( a = b & dom b = dom (Xn ^ X1) & ( for y being object st y in dom (Xn ^ X1) holds
b . y in (Xn ^ X1) . y ) )take b =
b;
( a = b & dom b = dom (Xn ^ X1) & ( for y being object st y in dom (Xn ^ X1) holds
b2 . b3 in (Xn ^ X1) . b3 ) )thus
a = b
by A102;
( dom b = dom (Xn ^ X1) & ( for y being object st y in dom (Xn ^ X1) holds
b2 . b3 in (Xn ^ X1) . b3 ) )
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;
for y being object st y in dom (Xn ^ X1) holds
b2 . b3 in (Xn ^ X1) . b3let y be
object ;
( y in dom (Xn ^ X1) implies b1 . b2 in (Xn ^ X1) . b2 )assume A110:
y in dom (Xn ^ X1)
;
b1 . b2 in (Xn ^ X1) . b2then 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;
end; hence
a in product (Xn ^ X1)
by CARD_3:def 5;
verum 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 for a being object st a in hn holds
a in product Xnlet a be
object ;
( a in hn implies a in product Xn )assume
a in hn
;
a in product Xnthen 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 ( dom b = dom Xn & ( for y being object st y in dom Xn holds
b . y in Xn . y ) )thus
dom b = dom Xn
by A122, A118b, FINSEQ_1:def 3, A97;
for y being object st y in dom Xn holds
b . y in Xn . ylet y be
object ;
( y in dom Xn implies b . y in Xn . y )assume A124:
y in dom Xn
;
b . y in Xn . ythen 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 16;
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;
verum end; hence
a in product Xn
by A121, CARD_3:def 5;
verum end;
then A129:
hn c= product Xn
;
reconsider h1 =
product <*(g . (n + 1))*> as
set ;
A130:
now for a being object st a in h1 holds
a in product X1let a be
object ;
( a in h1 implies a in product X1 )assume
a in h1
;
a in product X1then 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 ( dom b = dom X1 & ( for y being object st y in dom X1 holds
b . y in X1 . y ) )thus
dom b = dom X1
by A132, FINSEQ_1:def 8, A97;
for y being object st y in dom X1 holds
b . y in X1 . ylet y be
object ;
( y in dom X1 implies b . y in X1 . y )assume A135:
y in dom X1
;
b . y in X1 . ythen 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, 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;
verum end; hence
a in product X1
by A131, CARD_3:def 5;
verum end;
then
h1 c= product X1
;
then reconsider s12 =
[:hn,h1:] as
Subset of
[:(product Xn),(product X1):] by A129, ZFMISC_1:96;
now ( s12 in S12 & t1 = I .: s12 )now ( hn is Element of SemiringProduct Sn & h1 is Element of SemiringProduct S1 )hence
hn is
Element of
SemiringProduct Sn
by Def3;
h1 is Element of SemiringProduct S1now ( h1 = product <*(g . (n + 1))*> & <*(g . (n + 1))*> in product S1 )thus
h1 = product <*(g . (n + 1))*>
;
<*(g . (n + 1))*> in product S1now ( dom <*(g . (n + 1))*> = dom S1 & ( for b being object st b in dom S1 holds
<*(g . (n + 1))*> . b in S1 . b ) )thus
dom <*(g . (n + 1))*> = dom S1
by FINSEQ_1:def 8, A97;
for b being object st b in dom S1 holds
<*(g . (n + 1))*> . b in S1 . blet b be
object ;
( b in dom S1 implies <*(g . (n + 1))*> . b in S1 . b )assume
b in dom S1
;
<*(g . (n + 1))*> . b in S1 . bthen A144:
b = 1
by A97, FINSEQ_1:2, TARSKI:def 1;
(
<*(g . (n + 1))*> . 1
in (Sn ^ S1) . (n + 1) & 1
in dom S1 )
by A96, FINSEQ_1:4, A101, A97, FINSEQ_1:2, TARSKI:def 1;
hence
<*(g . (n + 1))*> . b in S1 . b
by A144, A99, FINSEQ_1:def 7;
verum end; hence
<*(g . (n + 1))*> in product S1
by CARD_3:def 5;
verum end; hence
h1 is
Element of
SemiringProduct S1
by Def3;
verum end; hence
s12 in S12
by A2b;
t1 = I .: s12now ( ( for u being object st u in I .: [:hn,h1:] holds
u in product f ) & ( for u being object st u in product f holds
u in I .: [:hn,h1:] ) )hereby for u being object st u in product f holds
u in I .: [:hn,h1:]
let u be
object ;
( u in I .: [:hn,h1:] implies u in product f )assume
u in I .: [:hn,h1:]
;
u in product fthen 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;
hence
u in product f
by A152, CARD_3:def 5;
verum
end; let u be
object ;
( u in product f implies u in I .: [:hn,h1:] )assume
u in product f
;
u in I .: [:hn,h1:]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 ( dom xn = dom Xn & ( for y being object st y in dom Xn holds
xn . y in Xn . y ) )
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;
for y being object st y in dom Xn holds
xn . y in Xn . ylet y be
object ;
( y in dom Xn implies xn . y in Xn . y )assume A175:
y in dom Xn
;
xn . y in Xn . yA176:
(
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;
verum end;
hence
xn in product Xn
by CARD_3:def 5;
x1 in product X1
now ( dom x1 = dom X1 & ( for y being object st y in dom X1 holds
x1 . y in X1 . y ) )thus
dom x1 = dom X1
by A97, FINSEQ_1:def 8;
for y being object st y in dom X1 holds
x1 . y in X1 . ylet y be
object ;
( y in dom X1 implies x1 . y in X1 . y )assume
y in dom X1
;
x1 . y in X1 . ythen A181:
y = 1
by A97, 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
(
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;
verum end;
hence
x1 in product X1
by CARD_3:def 5;
verum
end; set x =
[xn,x1];
now ( [xn,x1] in dom I & [xn,x1] in [:hn,h1:] & u = I . [xn,x1] )
dom I = [:(product Xn),(product X1):]
by FUNCT_2:def 1;
hence
[xn,x1] in dom I
by A172, ZFMISC_1:def 2;
( [xn,x1] in [:hn,h1:] & u = I . [xn,x1] )now ( xn in hn & x1 in h1 & [xn,x1] = [xn,x1] )now ( dom (v | (Seg n)) = dom (g | n) & ( for y being object st y in dom (g | n) holds
(v | (Seg n)) . y in (g | n) . y ) )
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;
for y being object st y in dom (g | n) holds
(v | (Seg n)) . y in (g | n) . ylet y be
object ;
( y in dom (g | n) implies (v | (Seg n)) . y in (g | n) . y )assume A186:
y in dom (g | n)
;
(v | (Seg n)) . y in (g | n) . ythen 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 16;
verum end; hence
xn in hn
by CARD_3:def 5;
( x1 in h1 & [xn,x1] = [xn,x1] )hence
x1 in h1
by CARD_3:def 5;
[xn,x1] = [xn,x1]thus
[xn,x1] = [xn,x1]
;
verum hence
[xn,x1] in [:hn,h1:]
by ZFMISC_1:def 2;
u = I . [xn,x1]hence
u = I . [xn,x1]
by A166;
verum end; hence
u in I .: [:hn,h1:]
by FUNCT_1:def 6;
verum then
(
I .: [:hn,h1:] c= product f &
product f c= I .: [:hn,h1:] )
;
hence
t1 = I .: s12
by A92;
verum
hence
t in I .: S12
by FUNCT_2:def 10;
verum
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; verum