let o1, o2 be non empty Ordinal; for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic
set P2 = Polynom-Ring ((o1 +^ o2),L);
set P1 = Polynom-Ring (o1,(Polynom-Ring (o2,L)));
defpred S1[ set , set ] means for P being Polynomial of o1,(Polynom-Ring (o2,L)) st $1 = P holds
$2 = Compress P;
reconsider 1P1 = 1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) as Polynomial of o1,(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider 1P2 = 1_ (Polynom-Ring ((o1 +^ o2),L)) as Polynomial of (o1 +^ o2),L by POLYNOM1:def 11;
A1:
for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S1[x,u]
proof
let x be
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L))));
ex u being Element of (Polynom-Ring ((o1 +^ o2),L)) st S1[x,u]
reconsider Q =
x as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider u =
Compress Q as
Element of
(Polynom-Ring ((o1 +^ o2),L)) by POLYNOM1:def 11;
take
u
;
S1[x,u]
let P be
Polynomial of
o1,
(Polynom-Ring (o2,L));
( x = P implies u = Compress P )
assume
x = P
;
u = Compress P
hence
u = Compress P
;
verum
end;
consider f being Function of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L)) such that
A2:
for x being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
reconsider f = f as Function of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))),(Polynom-Ring ((o1 +^ o2),L)) ;
take
f
; QUOFIELD:def 23 f is RingIsomorphism
thus
f is additive
RINGCAT1:def 1,MOD_4:def 8,MOD_4:def 12 ( f is multiplicative & f is unity-preserving & f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )proof
let x,
y be
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L))));
VECTSP_1:def 19 f . (x + y) = (f . x) + (f . y)
reconsider x9 =
x,
y9 =
y as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p =
x9,
q =
y9 as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider fp =
f . x,
fq =
f . y,
fpq =
f . (x + y) as
Element of
(Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp =
fp,
fq =
fq,
fpq =
fpq as
Polynomial of
(o1 +^ o2),
L by POLYNOM1:def 11;
for
x being
bag of
o1 +^ o2 holds
fpq . x = (fp . x) + (fq . x)
proof
let b be
bag of
o1 +^ o2;
fpq . b = (fp . b) + (fq . b)
reconsider b9 =
b as
Element of
Bags (o1 +^ o2) by PRE_POLY:def 12;
consider b1 being
Element of
Bags o1,
b2 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A3:
Q1 = p . b1
and A4:
b9 = b1 +^ b2
and A5:
(Compress p) . b9 = Q1 . b2
by Def2;
consider b19 being
Element of
Bags o1,
b29 being
Element of
Bags o2,
Q19 being
Polynomial of
o2,
L such that A6:
Q19 = q . b19
and A7:
b9 = b19 +^ b29
and A8:
(Compress q) . b9 = Q19 . b29
by Def2;
consider b199 being
Element of
Bags o1,
b299 being
Element of
Bags o2,
Q199 being
Polynomial of
o2,
L such that A9:
Q199 = (p + q) . b199
and A10:
b9 = b199 +^ b299
and A11:
(Compress (p + q)) . b9 = Q199 . b299
by Def2;
A12:
b19 = b199
by A7, A10, Th7;
reconsider b1 =
b1 as
bag of
o1 ;
A13:
(p + q) . b1 = (p . b1) + (q . b1)
by POLYNOM1:15;
b1 = b19
by A4, A7, Th7;
then
Q199 = Q1 + Q19
by A3, A6, A9, A12, A13, POLYNOM1:def 11;
then A14:
Q199 . b2 = (Q1 . b2) + (Q19 . b2)
by POLYNOM1:15;
A15:
b29 = b299
by A7, A10, Th7;
A16:
b2 = b29
by A4, A7, Th7;
x + y = p + q
by POLYNOM1:def 11;
hence fpq . b =
(Compress (p + q)) . b9
by A2
.=
((Compress p) . b9) + (fq . b)
by A2, A5, A8, A11, A16, A15, A14
.=
(fp . b) + (fq . b)
by A2
;
verum
end;
hence f . (x + y) =
fp + fq
by POLYNOM1:16
.=
(f . x) + (f . y)
by POLYNOM1:def 11
;
verum
end;
now for x, y being Element of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) holds f . (x * y) = (f . x) * (f . y)let x,
y be
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L))));
f . (x * y) = (f . x) * (f . y)reconsider x9 =
x,
y9 =
y as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) ;
reconsider p =
x9,
q =
y9 as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider fp =
f . x,
fq =
f . y as
Element of
(Polynom-Ring ((o1 +^ o2),L)) ;
reconsider fp =
fp,
fq =
fq as
Polynomial of
(o1 +^ o2),
L by POLYNOM1:def 11;
f . (x * y) = f . (p *' q)
by POLYNOM1:def 11;
then reconsider fpq9 =
f . (p *' q) as
Polynomial of
(o1 +^ o2),
L by POLYNOM1:def 11;
A17:
for
b being
bag of
o1 +^ o2 ex
s being
FinSequence of the
carrier of
L st
(
fpq9 . b = Sum s &
len s = len (decomp b) & ( for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of
o1 +^ o2 st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (fp . b1) * (fq . b2) ) ) )
proof
reconsider x =
p *' q as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def 11;
let c be
bag of
o1 +^ o2;
ex s being FinSequence of the carrier of L st
( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
reconsider b =
c as
Element of
Bags (o1 +^ o2) by PRE_POLY:def 12;
consider b1 being
Element of
Bags o1,
b2 being
Element of
Bags o2 such that A18:
b = b1 +^ b2
by Th6;
reconsider b1 =
b1 as
bag of
o1 ;
consider r being
FinSequence of the
carrier of
(Polynom-Ring (o2,L)) such that A19:
(p *' q) . b1 = Sum r
and A20:
len r = len (decomp b1)
and A21:
for
k being
Element of
NAT st
k in dom r holds
ex
a19,
b19 being
bag of
o1 st
(
(decomp b1) /. k = <*a19,b19*> &
r /. k = (p . a19) * (q . b19) )
by POLYNOM1:def 10;
for
x being
object st
x in dom r holds
r . x is
Function
then reconsider rFF =
r as
Function-yielding Function by FUNCOP_1:def 6;
deffunc H1(
object )
-> set =
(rFF . $1) . b2;
consider rFFb2 being
Function such that A23:
dom rFFb2 = dom r
and A24:
for
i being
object st
i in dom r holds
rFFb2 . i = H1(
i)
from FUNCT_1:sch 3();
ex
i being
Nat st
dom r = Seg i
by FINSEQ_1:def 2;
then reconsider rFFb2 =
rFFb2 as
FinSequence by A23, FINSEQ_1:def 2;
A25:
rng rFFb2 c= the
carrier of
L
proof
let u be
object ;
TARSKI:def 3 ( not u in rng rFFb2 or u in the carrier of L )
A26:
rng rFF c= the
carrier of
(Polynom-Ring (o2,L))
by FINSEQ_1:def 4;
assume
u in rng rFFb2
;
u in the carrier of L
then consider x being
object such that A27:
x in dom rFFb2
and A28:
u = rFFb2 . x
by FUNCT_1:def 3;
rFF . x in rng rFF
by A23, A27, FUNCT_1:3;
then A29:
rFF . x is
Function of
(Bags o2), the
carrier of
L
by A26, POLYNOM1:def 11;
then A30:
rng (rFF . x) c= the
carrier of
L
by RELAT_1:def 19;
dom (rFF . x) = Bags o2
by A29, FUNCT_2:def 1;
then A31:
(rFF . x) . b2 in rng (rFF . x)
by FUNCT_1:3;
rFFb2 . x = (rFF . x) . b2
by A23, A24, A27;
hence
u in the
carrier of
L
by A28, A30, A31;
verum
end;
defpred S2[
set ,
set ]
means ex
a19,
b19 being
bag of
o1 ex
Fk being
FinSequence of the
carrier of
L ex
pa19,
qb19 being
Polynomial of
o2,
L st
(
pa19 = p . a19 &
qb19 = q . b19 &
Fk = $2 &
(decomp b1) /. $1
= <*a19,b19*> &
len Fk = len (decomp b2) & ( for
m being
Nat st
m in dom Fk holds
ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) );
A32:
for
k being
Nat st
k in Seg (len r) holds
ex
x being
Element of the
carrier of
L * st
S2[
k,
x]
proof
let k be
Nat;
( k in Seg (len r) implies ex x being Element of the carrier of L * st S2[k,x] )
assume
k in Seg (len r)
;
ex x being Element of the carrier of L * st S2[k,x]
then
k in dom (decomp b1)
by A20, FINSEQ_1:def 3;
then consider a19,
b19 being
bag of
o1 such that A33:
(decomp b1) /. k = <*a19,b19*>
and
b1 = a19 + b19
by PRE_POLY:68;
reconsider pa199 =
p . a19,
qb199 =
q . b19 as
Element of
(Polynom-Ring (o2,L)) ;
reconsider pa19 =
pa199,
qb19 =
qb199 as
Polynomial of
o2,
L by POLYNOM1:def 11;
defpred S3[
set ,
set ]
means ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. $1
= <*a199,b199*> & $2
= (pa19 . a199) * (qb19 . b199) );
A34:
for
k being
Nat st
k in Seg (len (decomp b2)) holds
ex
x being
Element of
L st
S3[
k,
x]
consider Fk being
FinSequence of the
carrier of
L such that A36:
dom Fk = Seg (len (decomp b2))
and A37:
for
k being
Nat st
k in Seg (len (decomp b2)) holds
S3[
k,
Fk /. k]
from RECDEF_1:sch 17(A34);
reconsider x =
Fk as
Element of the
carrier of
L * by FINSEQ_1:def 11;
take
x
;
S2[k,x]
take
a19
;
ex b19 being bag of o1 ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take
b19
;
ex Fk being FinSequence of the carrier of L ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take
Fk
;
ex pa19, qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take
pa19
;
ex qb19 being Polynomial of o2,L st
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
take
qb19
;
( pa19 = p . a19 & qb19 = q . b19 & Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus
(
pa19 = p . a19 &
qb19 = q . b19 &
Fk = x )
;
( (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus
(decomp b1) /. k = <*a19,b19*>
by A33;
( len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) )
thus
len Fk = len (decomp b2)
by A36, FINSEQ_1:def 3;
for m being Nat st m in dom Fk holds
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )
let m be
Nat;
( m in dom Fk implies ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) ) )
assume
m in dom Fk
;
ex a199, b199 being bag of o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = (pa19 . a199) * (qb19 . b199) )
hence
ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = (pa19 . a199) * (qb19 . b199) )
by A36, A37;
verum
end;
consider F being
FinSequence of the
carrier of
L * such that A38:
dom F = Seg (len r)
and A39:
for
k being
Nat st
k in Seg (len r) holds
S2[
k,
F /. k]
from RECDEF_1:sch 17(A32);
take s =
FlattenSeq F;
( fpq9 . c = Sum s & len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
A40:
len (Sum F) = len F
by MATRLIN:def 6;
reconsider rFFb2 =
rFFb2 as
FinSequence of the
carrier of
L by A25, FINSEQ_1:def 4;
A41:
f . x = Compress (p *' q)
by A2;
A42:
dom rFFb2 =
dom F
by A38, A23, FINSEQ_1:def 3
.=
dom (Sum F)
by A40, FINSEQ_3:29
;
for
k being
Nat st
k in dom rFFb2 holds
rFFb2 . k = (Sum F) . k
proof
let k be
Nat;
( k in dom rFFb2 implies rFFb2 . k = (Sum F) . k )
assume A43:
k in dom rFFb2
;
rFFb2 . k = (Sum F) . k
consider c1,
d1 being
bag of
o1 such that A44:
(decomp b1) /. k = <*c1,d1*>
and A45:
r /. k = (p . c1) * (q . d1)
by A21, A23, A43;
k in Seg (len r)
by A23, A43, FINSEQ_1:def 3;
then consider a19,
b19 being
bag of
o1,
Fk being
FinSequence of the
carrier of
L,
pa19,
qb19 being
Polynomial of
o2,
L such that A46:
(
pa19 = p . a19 &
qb19 = q . b19 )
and A47:
Fk = F /. k
and A48:
(decomp b1) /. k = <*a19,b19*>
and A49:
len Fk = len (decomp b2)
and A50:
for
ki being
Nat st
ki in dom Fk holds
ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. ki = <*a199,b199*> &
Fk /. ki = (pa19 . a199) * (qb19 . b199) )
by A39;
A51:
(
c1 = a19 &
d1 = b19 )
by A44, A48, FINSEQ_1:77;
consider s1 being
FinSequence of the
carrier of
L such that A52:
(pa19 *' qb19) . b2 = Sum s1
and A53:
len s1 = len (decomp b2)
and A54:
for
ki being
Element of
NAT st
ki in dom s1 holds
ex
x1,
y2 being
bag of
o2 st
(
(decomp b2) /. ki = <*x1,y2*> &
s1 /. ki = (pa19 . x1) * (qb19 . y2) )
by POLYNOM1:def 10;
A55:
dom s1 = Seg (len s1)
by FINSEQ_1:def 3;
now for ki being Nat st ki in dom s1 holds
s1 . ki = Fk . kilet ki be
Nat;
( ki in dom s1 implies s1 . ki = Fk . ki )assume A56:
ki in dom s1
;
s1 . ki = Fk . kithen A57:
s1 /. ki = s1 . ki
by PARTFUN1:def 6;
A58:
ki in dom Fk
by A49, A53, A55, A56, FINSEQ_1:def 3;
then consider a199,
b199 being
bag of
o2 such that A59:
(decomp b2) /. ki = <*a199,b199*>
and A60:
Fk /. ki = (pa19 . a199) * (qb19 . b199)
by A50;
consider x1,
y2 being
bag of
o2 such that A61:
(decomp b2) /. ki = <*x1,y2*>
and A62:
s1 /. ki = (pa19 . x1) * (qb19 . y2)
by A54, A56;
(
x1 = a199 &
y2 = b199 )
by A61, A59, FINSEQ_1:77;
hence
s1 . ki = Fk . ki
by A62, A58, A60, A57, PARTFUN1:def 6;
verum end;
then A63:
s1 = Fk
by A49, A53, FINSEQ_2:9;
A64:
rFF . k =
r /. k
by A23, A43, PARTFUN1:def 6
.=
pa19 *' qb19
by A45, A46, A51, POLYNOM1:def 11
;
thus rFFb2 . k =
(rFF . k) . b2
by A23, A24, A43
.=
(Sum F) /. k
by A42, A43, A47, A64, A52, A63, MATRLIN:def 6
.=
(Sum F) . k
by A42, A43, PARTFUN1:def 6
;
verum
end;
then A65:
rFFb2 = Sum F
by A42;
reconsider Sr =
Sum r as
Polynomial of
o2,
L by POLYNOM1:def 11;
consider gg being
sequence of the
carrier of
(Polynom-Ring (o2,L)) such that A66:
Sum r = gg . (len r)
and A67:
gg . 0 = 0. (Polynom-Ring (o2,L))
and A68:
for
j being
Nat for
v being
Element of
(Polynom-Ring (o2,L)) st
j < len r &
v = r . (j + 1) holds
gg . (j + 1) = (gg . j) + v
by RLVECT_1:def 12;
defpred S3[
Nat,
set ]
means for
pp being
Polynomial of
o2,
L st $1
<= len r &
pp = gg . $1 holds
$2
= pp . b2;
A69:
for
x being
Element of
NAT ex
y being
Element of
L st
S3[
x,
y]
consider ff being
sequence of the
carrier of
L such that A71:
for
j being
Element of
NAT holds
S3[
j,
ff . j]
from FUNCT_2:sch 3(A69);
A72:
for
j being
Nat holds
S3[
j,
ff . j]
defpred S4[
set ,
set ]
means ex
a19,
b19 being
Element of
Bags o1 ex
Fk being
FinSequence of 2
-tuples_on (Bags (o1 +^ o2)) st
(
Fk = $2 &
(decomp b1) /. $1
= <*a19,b19*> &
len Fk = len (decomp b2) & ( for
m being
Nat st
m in dom Fk holds
ex
a199,
b199 being
Element of
Bags o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) );
A73:
for
i being
Nat st
i in Seg (len r) holds
ex
x being
Element of
(2 -tuples_on (Bags (o1 +^ o2))) * st
S4[
i,
x]
proof
let k be
Nat;
( k in Seg (len r) implies ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S4[k,x] )
assume
k in Seg (len r)
;
ex x being Element of (2 -tuples_on (Bags (o1 +^ o2))) * st S4[k,x]
then
k in dom (decomp b1)
by A20, FINSEQ_1:def 3;
then consider a19,
b19 being
bag of
o1 such that A74:
(decomp b1) /. k = <*a19,b19*>
and
b1 = a19 + b19
by PRE_POLY:68;
reconsider a19 =
a19,
b19 =
b19 as
Element of
Bags o1 by PRE_POLY:def 12;
defpred S5[
set ,
set ]
means ex
a199,
b199 being
Element of
Bags o2 st
(
(decomp b2) /. $1
= <*a199,b199*> & $2
= <*(a19 +^ a199),(b19 +^ b199)*> );
A75:
for
k being
Nat st
k in Seg (len (decomp b2)) holds
ex
x being
Element of 2
-tuples_on (Bags (o1 +^ o2)) st
S5[
k,
x]
proof
let k be
Nat;
( k in Seg (len (decomp b2)) implies ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S5[k,x] )
assume
k in Seg (len (decomp b2))
;
ex x being Element of 2 -tuples_on (Bags (o1 +^ o2)) st S5[k,x]
then
k in dom (decomp b2)
by FINSEQ_1:def 3;
then consider a199,
b199 being
bag of
o2 such that A76:
(decomp b2) /. k = <*a199,b199*>
and
b2 = a199 + b199
by PRE_POLY:68;
reconsider a199 =
a199,
b199 =
b199 as
Element of
Bags o2 by PRE_POLY:def 12;
reconsider x =
<*(a19 +^ a199),(b19 +^ b199)*> as
Element of 2
-tuples_on (Bags (o1 +^ o2)) ;
take
x
;
S5[k,x]
take
a199
;
ex b199 being Element of Bags o2 st
( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )
take
b199
;
( (decomp b2) /. k = <*a199,b199*> & x = <*(a19 +^ a199),(b19 +^ b199)*> )
thus
(
(decomp b2) /. k = <*a199,b199*> &
x = <*(a19 +^ a199),(b19 +^ b199)*> )
by A76;
verum
end;
consider Fk being
FinSequence of 2
-tuples_on (Bags (o1 +^ o2)) such that A77:
dom Fk = Seg (len (decomp b2))
and A78:
for
k being
Nat st
k in Seg (len (decomp b2)) holds
S5[
k,
Fk /. k]
from RECDEF_1:sch 17(A75);
reconsider x =
Fk as
Element of
(2 -tuples_on (Bags (o1 +^ o2))) * by FINSEQ_1:def 11;
take
x
;
S4[k,x]
take
a19
;
ex b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
take
b19
;
ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
take
Fk
;
( Fk = x & (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus
Fk = x
;
( (decomp b1) /. k = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus
(decomp b1) /. k = <*a19,b19*>
by A74;
( len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) )
thus
len Fk = len (decomp b2)
by A77, FINSEQ_1:def 3;
for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )
let m be
Nat;
( m in dom Fk implies ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) )
assume
m in dom Fk
;
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )
hence
ex
a199,
b199 being
Element of
Bags o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> )
by A77, A78;
verum
end;
consider G being
FinSequence of
(2 -tuples_on (Bags (o1 +^ o2))) * such that A79:
dom G = Seg (len r)
and A80:
for
i being
Nat st
i in Seg (len r) holds
S4[
i,
G /. i]
from RECDEF_1:sch 17(A73);
A81:
for
i being
Nat st
i in Seg (len r) holds
S4[
i,
G /. i]
by A80;
A82:
dom (Card F) = dom F
by CARD_3:def 2;
A83:
for
j being
Nat st
j in dom (Card F) holds
(Card F) . j = (Card G) . j
proof
let j be
Nat;
( j in dom (Card F) implies (Card F) . j = (Card G) . j )
assume A84:
j in dom (Card F)
;
(Card F) . j = (Card G) . j
then A85:
j in dom F
by CARD_3:def 2;
then A86:
(Card F) . j = card (F . j)
by CARD_3:def 2;
A87:
( ex
a19,
b19 being
bag of
o1 ex
Fk being
FinSequence of the
carrier of
L ex
pa19,
qb19 being
Polynomial of
o2,
L st
(
pa19 = p . a19 &
qb19 = q . b19 &
Fk = F /. j &
(decomp b1) /. j = <*a19,b19*> &
len Fk = len (decomp b2) & ( for
m being
Nat st
m in dom Fk holds
ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = (pa19 . a199) * (qb19 . b199) ) ) ) & ex
a29,
b29 being
Element of
Bags o1 ex
Gk being
FinSequence of 2
-tuples_on (Bags (o1 +^ o2)) st
(
Gk = G /. j &
(decomp b1) /. j = <*a29,b29*> &
len Gk = len (decomp b2) & ( for
m being
Nat st
m in dom Gk holds
ex
a299,
b299 being
Element of
Bags o2 st
(
(decomp b2) /. m = <*a299,b299*> &
Gk /. m = <*(a29 +^ a299),(b29 +^ b299)*> ) ) ) )
by A38, A39, A80, A85;
card (F . j) =
card (F /. j)
by A85, PARTFUN1:def 6
.=
card (G . j)
by A38, A79, A82, A84, A87, PARTFUN1:def 6
;
hence
(Card F) . j = (Card G) . j
by A38, A79, A82, A84, A86, CARD_3:def 2;
verum
end;
consider c1 being
Element of
Bags o1,
c2 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A88:
Q1 = (p *' q) . c1
and A89:
b = c1 +^ c2
and A90:
(Compress (p *' q)) . b = Q1 . c2
by Def2;
A91:
c1 = b1
by A18, A89, Th7;
then
dom G = dom (decomp c1)
by A20, A79, FINSEQ_1:def 3;
then A92:
decomp c = FlattenSeq G
by A18, A79, A81, A91, Th14;
A93:
for
j being
Nat for
v being
Element of
L st
j < len rFFb2 &
v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + v
proof
let j be
Nat;
for v being Element of L st j < len rFFb2 & v = rFFb2 . (j + 1) holds
ff . (j + 1) = (ff . j) + vlet v be
Element of
L;
( j < len rFFb2 & v = rFFb2 . (j + 1) implies ff . (j + 1) = (ff . j) + v )
assume that A94:
j < len rFFb2
and A95:
v = rFFb2 . (j + 1)
;
ff . (j + 1) = (ff . j) + v
reconsider w =
r /. (j + 1),
pp =
gg . j,
pp9 =
gg . (j + 1) as
Polynomial of
o2,
L by POLYNOM1:def 11;
reconsider w1 =
w,
pp1 =
pp,
pp19 =
pp9 as
Element of
(Polynom-Ring (o2,L)) ;
reconsider w1 =
w1,
pp1 =
pp1,
pp19 =
pp19 as
Element of
(Polynom-Ring (o2,L)) ;
A96:
j < len r
by A23, A94, FINSEQ_3:29;
then A97:
j + 1
<= len r
by NAT_1:13;
then A98:
w = r . (j + 1)
by FINSEQ_4:15, NAT_1:11;
then A99:
pp19 = pp1 + w1
by A68, A96;
1
<= j + 1
by NAT_1:11;
then
j + 1
in dom r
by A97, FINSEQ_3:25;
then A100:
w . b2 = v
by A24, A95, A98;
j + 1
<= len r
by A96, NAT_1:13;
hence ff . (j + 1) =
pp9 . b2
by A72
.=
(pp + w) . b2
by A99, POLYNOM1:def 11
.=
(pp . b2) + (w . b2)
by POLYNOM1:15
.=
(ff . j) + v
by A72, A96, A100
;
verum
end;
gg . 0 = 0_ (
o2,
L)
by A67, POLYNOM1:def 11;
then A101:
ff . 0 =
(0_ (o2,L)) . b2
by A72, NAT_1:2
.=
0. L
by POLYNOM1:22
;
len rFFb2 = len r
by A23, FINSEQ_3:29;
then
Sr . b2 = ff . (len rFFb2)
by A66, A72;
then A102:
Sr . b2 = Sum rFFb2
by A101, A93, RLVECT_1:def 12;
(
b1 = c1 &
b2 = c2 )
by A18, A89, Th7;
hence
fpq9 . c = Sum s
by A19, A88, A90, A65, A102, A41, POLYNOM1:14;
( len s = len (decomp c) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) ) )
dom (Card G) = dom G
by CARD_3:def 2;
then
len (Card F) = len (Card G)
by A38, A79, A82, FINSEQ_3:29;
then A103:
Card F = Card G
by A83, FINSEQ_2:9;
hence A104:
len s = len (decomp c)
by A92, PRE_POLY:28;
for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )
let k be
Element of
NAT ;
( k in dom s implies ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) ) )
assume A105:
k in dom s
;
ex b1, b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*b1,b2*> & s /. k = (fp . b1) * (fq . b2) )
then consider i,
j being
Nat such that A106:
i in dom F
and A107:
j in dom (F . i)
and A108:
k = (Sum (Card (F | (i -' 1)))) + j
and A109:
(F . i) . j = (FlattenSeq F) . k
by PRE_POLY:29;
A110:
k in dom (decomp c)
by A104, A105, FINSEQ_3:29;
then consider i9,
j9 being
Nat such that A111:
i9 in dom G
and A112:
j9 in dom (G . i9)
and A113:
k = (Sum (Card (G | (i9 -' 1)))) + j9
and A114:
(G . i9) . j9 = (decomp c) . k
by A92, PRE_POLY:29;
(Sum ((Card F) | (i -' 1))) + j =
(Sum (Card (F | (i -' 1)))) + j
by POLYNOM3:16
.=
(Sum ((Card G) | (i9 -' 1))) + j9
by A108, A113, POLYNOM3:16
;
then A115:
(
i = i9 &
j = j9 )
by A103, A106, A107, A111, A112, POLYNOM3:22;
consider c1,
c2 being
bag of
o1 +^ o2 such that A116:
(decomp c) /. k = <*c1,c2*>
and
c = c1 + c2
by A110, PRE_POLY:68;
reconsider cc1 =
c1,
cc2 =
c2 as
Element of
Bags (o1 +^ o2) by PRE_POLY:def 12;
consider cb1 being
Element of
Bags o1,
cb2 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A117:
Q1 = p . cb1
and A118:
cc1 = cb1 +^ cb2
and A119:
(Compress p) . cc1 = Q1 . cb2
by Def2;
consider a19,
b19 being
bag of
o1,
Fk being
FinSequence of the
carrier of
L,
pa19,
qb19 being
Polynomial of
o2,
L such that A120:
pa19 = p . a19
and A121:
qb19 = q . b19
and A122:
Fk = F /. i
and A123:
(decomp b1) /. i = <*a19,b19*>
and
len Fk = len (decomp b2)
and A124:
for
m being
Nat st
m in dom Fk holds
ex
a199,
b199 being
bag of
o2 st
(
(decomp b2) /. m = <*a199,b199*> &
Fk /. m = (pa19 . a199) * (qb19 . b199) )
by A38, A39, A106;
consider ga19,
gb19 being
Element of
Bags o1,
Gk being
FinSequence of 2
-tuples_on (Bags (o1 +^ o2)) such that A125:
Gk = G /. i
and A126:
(decomp b1) /. i = <*ga19,gb19*>
and
len Gk = len (decomp b2)
and A127:
for
m being
Nat st
m in dom Gk holds
ex
ga199,
gb199 being
Element of
Bags o2 st
(
(decomp b2) /. m = <*ga199,gb199*> &
Gk /. m = <*(ga19 +^ ga199),(gb19 +^ gb199)*> )
by A38, A80, A106;
A128:
b19 = gb19
by A123, A126, FINSEQ_1:77;
A129:
Gk = G . i
by A38, A79, A106, A125, PARTFUN1:def 6;
then consider ga199,
gb199 being
Element of
Bags o2 such that A130:
(decomp b2) /. j = <*ga199,gb199*>
and A131:
Gk /. j = <*(ga19 +^ ga199),(gb19 +^ gb199)*>
by A112, A115, A127;
A132:
<*c1,c2*> =
(G . i) . j
by A110, A116, A114, A115, PARTFUN1:def 6
.=
<*(ga19 +^ ga199),(gb19 +^ gb199)*>
by A112, A115, A129, A131, PARTFUN1:def 6
;
then
c1 = ga19 +^ ga199
by FINSEQ_1:77;
then A133:
(
cb1 = ga19 &
cb2 = ga199 )
by A118, Th7;
A134:
a19 = ga19
by A123, A126, FINSEQ_1:77;
j in dom Fk
by A106, A107, A122, PARTFUN1:def 6;
then consider a199,
b199 being
bag of
o2 such that A135:
(decomp b2) /. j = <*a199,b199*>
and A136:
Fk /. j = (pa19 . a199) * (qb19 . b199)
by A124;
a199 = ga199
by A130, A135, FINSEQ_1:77;
then A137:
pa19 . a199 = fp . c1
by A2, A120, A117, A119, A133, A134;
take
c1
;
ex b2 being bag of o1 +^ o2 st
( (decomp c) /. k = <*c1,b2*> & s /. k = (fp . c1) * (fq . b2) )
take
c2
;
( (decomp c) /. k = <*c1,c2*> & s /. k = (fp . c1) * (fq . c2) )
thus
(decomp c) /. k = <*c1,c2*>
by A116;
s /. k = (fp . c1) * (fq . c2)
consider cb1 being
Element of
Bags o1,
cb2 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A138:
Q1 = q . cb1
and A139:
cc2 = cb1 +^ cb2
and A140:
(Compress q) . cc2 = Q1 . cb2
by Def2;
c2 = gb19 +^ gb199
by A132, FINSEQ_1:77;
then A141:
(
cb1 = gb19 &
cb2 = gb199 )
by A139, Th7;
A142:
Fk = F . i
by A106, A122, PARTFUN1:def 6;
b199 = gb199
by A130, A135, FINSEQ_1:77;
then A143:
qb19 . b199 = fq . c2
by A2, A121, A128, A138, A140, A141;
thus s /. k =
s . k
by A105, PARTFUN1:def 6
.=
(fp . c1) * (fq . c2)
by A107, A109, A142, A136, A137, A143, PARTFUN1:def 6
;
verum
end; thus f . (x * y) =
f . (p *' q)
by POLYNOM1:def 11
.=
fp *' fq
by A17, POLYNOM1:def 10
.=
(f . x) * (f . y)
by POLYNOM1:def 11
;
verum end;
hence
f is multiplicative
by GROUP_6:def 6; ( f is unity-preserving & f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )
A144:
for b being Element of Bags (o1 +^ o2) holds (Compress 1P1) . b = 1P2 . b
proof
let b be
Element of
Bags (o1 +^ o2);
(Compress 1P1) . b = 1P2 . b
A145:
1P2 . b = (1_ ((o1 +^ o2),L)) . b
by POLYNOM1:31;
consider b1 being
Element of
Bags o1,
b2 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A146:
Q1 = 1P1 . b1
and A147:
b = b1 +^ b2
and A148:
(Compress 1P1) . b = Q1 . b2
by Def2;
per cases
( b = EmptyBag (o1 +^ o2) or b <> EmptyBag (o1 +^ o2) )
;
suppose A149:
b = EmptyBag (o1 +^ o2)
;
(Compress 1P1) . b = 1P2 . bthen A150:
b1 = EmptyBag o1
by A147, Th5;
A151:
b2 = EmptyBag o2
by A147, A149, Th5;
Q1 =
(1_ (o1,(Polynom-Ring (o2,L)))) . b1
by A146, POLYNOM1:31
.=
1_ (Polynom-Ring (o2,L))
by A150, POLYNOM1:25
;
then Q1 . b2 =
(1_ (o2,L)) . b2
by POLYNOM1:31
.=
1_ L
by A151, POLYNOM1:25
.=
1P2 . b
by A145, A149, POLYNOM1:25
;
hence
(Compress 1P1) . b = 1P2 . b
by A148;
verum end; suppose A152:
b <> EmptyBag (o1 +^ o2)
;
(Compress 1P1) . b = 1P2 . bthen A153:
(
b1 <> EmptyBag o1 or
b2 <> EmptyBag o2 )
by A147, Th5;
now (Compress 1P1) . b = 1P2 . bper cases
( b1 = EmptyBag o1 or b1 <> EmptyBag o1 )
;
suppose A154:
b1 = EmptyBag o1
;
(Compress 1P1) . b = 1P2 . bQ1 =
(1_ (o1,(Polynom-Ring (o2,L)))) . b1
by A146, POLYNOM1:31
.=
1_ (Polynom-Ring (o2,L))
by A154, POLYNOM1:25
.=
1_ (
o2,
L)
by POLYNOM1:31
;
then Q1 . b2 =
0. L
by A153, A154, POLYNOM1:25
.=
1P2 . b
by A145, A152, POLYNOM1:25
;
hence
(Compress 1P1) . b = 1P2 . b
by A148;
verum end; hence
(Compress 1P1) . b = 1P2 . b
;
verum end;
end;
f . (1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L))))) =
Compress 1P1
by A2
.=
1_ (Polynom-Ring ((o1 +^ o2),L))
by A144, FUNCT_2:63
;
hence
f is unity-preserving
by GROUP_1:def 13; ( f is one-to-one & f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L))) )
thus
f is one-to-one
f is V32( the carrier of (Polynom-Ring ((o1 +^ o2),L)))proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume
x1 in dom f
;
( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
then reconsider x19 =
x1 as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def 1;
assume
x2 in dom f
;
( not f . x1 = f . x2 or x1 = x2 )
then reconsider x29 =
x2 as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by FUNCT_2:def 1;
reconsider x299 =
x29 as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider x199 =
x19 as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
A156:
f . x29 = Compress x299
by A2;
then reconsider w2 =
f . x29 as
Polynomial of
(o1 +^ o2),
L ;
A157:
f . x19 = Compress x199
by A2;
then reconsider w1 =
f . x19 as
Polynomial of
(o1 +^ o2),
L ;
assume A158:
f . x1 = f . x2
;
x1 = x2
now for b1 being Element of Bags o1 holds x199 . b1 = x299 . b1let b1 be
Element of
Bags o1;
x199 . b1 = x299 . b1reconsider x199b1 =
x199 . b1,
x299b1 =
x299 . b1 as
Polynomial of
o2,
L by POLYNOM1:def 11;
now for b2 being Element of Bags o2 holds x199b1 . b2 = x299b1 . b2let b2 be
Element of
Bags o2;
x199b1 . b2 = x299b1 . b2set b =
b1 +^ b2;
consider b19 being
Element of
Bags o1,
b29 being
Element of
Bags o2,
Q1 being
Polynomial of
o2,
L such that A159:
Q1 = x199 . b19
and A160:
b1 +^ b2 = b19 +^ b29
and A161:
w1 . (b1 +^ b2) = Q1 . b29
by A157, Def2;
A162:
(
b1 = b19 &
b2 = b29 )
by A160, Th7;
consider c1 being
Element of
Bags o1,
c2 being
Element of
Bags o2,
Q19 being
Polynomial of
o2,
L such that A163:
Q19 = x299 . c1
and A164:
b1 +^ b2 = c1 +^ c2
and A165:
w2 . (b1 +^ b2) = Q19 . c2
by A156, Def2;
b1 = c1
by A164, Th7;
hence
x199b1 . b2 = x299b1 . b2
by A158, A159, A161, A163, A164, A165, A162, Th7;
verum end; hence
x199 . b1 = x299 . b1
by FUNCT_2:63;
verum end;
hence
x1 = x2
by FUNCT_2:63;
verum
end;
thus
rng f c= the carrier of (Polynom-Ring ((o1 +^ o2),L))
by RELAT_1:def 19; XBOOLE_0:def 10,FUNCT_2:def 3 the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= K734( the carrier of (Polynom-Ring ((o1 +^ o2),L)),f)
thus
the carrier of (Polynom-Ring ((o1 +^ o2),L)) c= rng f
verumproof
defpred S2[
set ,
set ]
means ex
b1 being
Element of
Bags o1 ex
b2 being
Element of
Bags o2 st
( $1
= b1 +^ b2 & $2
= b1 );
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (Polynom-Ring ((o1 +^ o2),L)) or y in rng f )
assume
y in the
carrier of
(Polynom-Ring ((o1 +^ o2),L))
;
y in rng f
then reconsider s =
y as
Polynomial of
(o1 +^ o2),
L by POLYNOM1:def 11;
defpred S3[
Element of
Bags o1,
Element of
(Polynom-Ring (o2,L))]
means ex
h being
Function st
(
h = $2 & ( for
b2 being
Element of
Bags o2 for
b being
Element of
Bags (o1 +^ o2) st
b = $1
+^ b2 holds
h . b2 = s . b ) );
A166:
for
x being
Element of
Bags (o1 +^ o2) ex
y being
Element of
Bags o1 st
S2[
x,
y]
consider kk being
Function of
(Bags (o1 +^ o2)),
(Bags o1) such that A168:
for
b being
Element of
Bags (o1 +^ o2) holds
S2[
b,
kk . b]
from FUNCT_2:sch 3(A166);
A169:
for
x being
Element of
Bags o1 ex
y being
Element of
(Polynom-Ring (o2,L)) st
S3[
x,
y]
proof
defpred S4[
set ,
set ]
means ex
b1 being
Element of
Bags o1 ex
b2 being
Element of
Bags o2 st
( $1
= b1 +^ b2 & $2
= b2 );
let x be
Element of
Bags o1;
ex y being Element of (Polynom-Ring (o2,L)) st S3[x,y]
reconsider b1 =
x as
Element of
Bags o1 ;
defpred S5[
Element of
Bags o2,
Element of
L]
means for
b being
Element of
Bags (o1 +^ o2) st
b = b1 +^ $1 holds
$2
= s . b;
A170:
for
p being
Element of
Bags o2 ex
q being
Element of
L st
S5[
p,
q]
consider t being
Function of
(Bags o2), the
carrier of
L such that A171:
for
b2 being
Element of
Bags o2 holds
S5[
b2,
t . b2]
from FUNCT_2:sch 3(A170);
reconsider t =
t as
Function of
(Bags o2),
L ;
A172:
for
x being
Element of
Bags (o1 +^ o2) ex
y being
Element of
Bags o2 st
S4[
x,
y]
consider kk being
Function of
(Bags (o1 +^ o2)),
(Bags o2) such that A174:
for
b being
Element of
Bags (o1 +^ o2) holds
S4[
b,
kk . b]
from FUNCT_2:sch 3(A172);
Support t c= kk .: (Support s)
then
t is
Polynomial of
o2,
L
by POLYNOM1:def 5;
then reconsider t99 =
t as
Element of
(Polynom-Ring (o2,L)) by POLYNOM1:def 11;
reconsider t9 =
t as
Function ;
take
t99
;
S3[x,t99]
take
t9
;
( t9 = t99 & ( for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . b ) )
thus
t99 = t9
;
for b2 being Element of Bags o2
for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . b
let b2 be
Element of
Bags o2;
for b being Element of Bags (o1 +^ o2) st b = x +^ b2 holds
t9 . b2 = s . blet b be
Element of
Bags (o1 +^ o2);
( b = x +^ b2 implies t9 . b2 = s . b )
assume
b = x +^ b2
;
t9 . b2 = s . b
hence
t9 . b2 = s . b
by A171;
verum
end;
consider g being
Function of
(Bags o1), the
carrier of
(Polynom-Ring (o2,L)) such that A177:
for
x being
Element of
Bags o1 holds
S3[
x,
g . x]
from FUNCT_2:sch 3(A169);
reconsider g =
g as
Function of
(Bags o1),
(Polynom-Ring (o2,L)) ;
A178:
Support g c= kk .: (Support s)
proof
let x be
object ;
TARSKI:def 3 ( not x in Support g or x in kk .: (Support s) )
assume A179:
x in Support g
;
x in kk .: (Support s)
then reconsider b1 =
x as
Element of
Bags o1 ;
consider h being
Function such that A180:
h = g . b1
and A181:
for
b2 being
Element of
Bags o2 for
b being
Element of
Bags (o1 +^ o2) st
b = b1 +^ b2 holds
h . b2 = s . b
by A177;
reconsider h =
h as
Polynomial of
o2,
L by A180, POLYNOM1:def 11;
g . b1 <> 0. (Polynom-Ring (o2,L))
by A179, POLYNOM1:def 4;
then
g . b1 <> 0_ (
o2,
L)
by POLYNOM1:def 11;
then consider b2 being
Element of
Bags o2 such that A182:
b2 in Support h
by A180, POLYNOM2:17, SUBSET_1:4;
set b =
b1 +^ b2;
h . b2 <> 0. L
by A182, POLYNOM1:def 4;
then
s . (b1 +^ b2) <> 0. L
by A181;
then A183:
(
dom kk = Bags (o1 +^ o2) &
b1 +^ b2 in Support s )
by FUNCT_2:def 1, POLYNOM1:def 4;
ex
b19 being
Element of
Bags o1 ex
b29 being
Element of
Bags o2 st
(
b1 +^ b2 = b19 +^ b29 &
kk . (b1 +^ b2) = b19 )
by A168;
then
x = kk . (b1 +^ b2)
by Th7;
hence
x in kk .: (Support s)
by A183, FUNCT_1:def 6;
verum
end;
then
g is
Polynomial of
o1,
(Polynom-Ring (o2,L))
by POLYNOM1:def 5;
then reconsider g =
g as
Element of
(Polynom-Ring (o1,(Polynom-Ring (o2,L)))) by POLYNOM1:def 11;
reconsider g9 =
g as
Polynomial of
o1,
(Polynom-Ring (o2,L)) by A178, POLYNOM1:def 5;
then A185:
y =
Compress g9
by FUNCT_2:63
.=
f . g
by A2
;
dom f = the
carrier of
(Polynom-Ring (o1,(Polynom-Ring (o2,L))))
by FUNCT_2:def 1;
hence
y in rng f
by A185, FUNCT_1:3;
verum
end;