let k, n, m be Nat; for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (q,XanyY) ) )
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; for p being Polynomial of (n + m),L ex q being Polynomial of ((n + k) + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (q,XanyY) ) )
let p be Polynomial of (n + m),L; ex q being Polynomial of ((n + k) + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (q,XanyY) ) )
consider P being Polynomial of ((n + m) + k),L such that
A1:
rng P c= (rng p) \/ {(0. L)}
and
A2:
for x being Function of (n + m),L
for y being Function of ((n + m) + k),L st y | (n + m) = x holds
eval (p,x) = eval (P,y)
by Th27;
reconsider P1 = P as Polynomial of ((n + k) + m),L ;
set I = id ((n + k) + m);
dom (id ((n + k) + m)) = (n + k) + m
;
then reconsider I = id ((n + k) + m) as XFinSequence by AFINSQ_1:5;
set nm = n + m;
set Inm = I | (n + m);
A3:
I = (I | (n + m)) ^ (I /^ (n + m))
;
A4:
I | (n + m) = ((I | (n + m)) | n) ^ ((I | (n + m)) /^ n)
;
A5:
rng I = (rng (I | (n + m))) \/ (rng (I /^ (n + m)))
by A3, AFINSQ_1:26;
A6:
rng (I | (n + m)) misses rng (I /^ (n + m))
by A3, Th1;
A7:
rng (I | (n + m)) = (rng ((I | (n + m)) | n)) \/ (rng ((I | (n + m)) /^ n))
by A4, AFINSQ_1:26;
A8:
rng ((I | (n + m)) | n) misses rng ((I | (n + m)) /^ n)
by A4, Th1;
rng ((I | (n + m)) | n) misses rng (I /^ (n + m))
by A6, XBOOLE_1:63, A7, XBOOLE_1:7;
then A9:
((I | (n + m)) | n) ^ (I /^ (n + m)) is one-to-one
by CARD_FIN:52;
A10:
rng (((I | (n + m)) | n) ^ (I /^ (n + m))) = (rng ((I | (n + m)) | n)) \/ (rng (I /^ (n + m)))
by AFINSQ_1:26;
rng (I /^ (n + m)) misses rng ((I | (n + m)) /^ n)
by A6, XBOOLE_1:63, A7, XBOOLE_1:7;
then
rng (((I | (n + m)) | n) ^ (I /^ (n + m))) misses rng ((I | (n + m)) /^ n)
by A10, A8, XBOOLE_1:70;
then A11:
(((I | (n + m)) | n) ^ (I /^ (n + m))) ^ ((I | (n + m)) /^ n) is one-to-one
by A9, CARD_FIN:52;
A12: rng ((((I | (n + m)) | n) ^ (I /^ (n + m))) ^ ((I | (n + m)) /^ n)) =
(rng (((I | (n + m)) | n) ^ (I /^ (n + m)))) \/ (rng ((I | (n + m)) /^ n))
by AFINSQ_1:26
.=
((rng ((I | (n + m)) | n)) \/ (rng (I /^ (n + m)))) \/ (rng ((I | (n + m)) /^ n))
by AFINSQ_1:26
.=
(n + k) + m
by A5, A7, XBOOLE_1:4
;
len ((((I | (n + m)) | n) ^ (I /^ (n + m))) ^ ((I | (n + m)) /^ n)) =
(len (((I | (n + m)) | n) ^ (I /^ (n + m)))) + (len ((I | (n + m)) /^ n))
by AFINSQ_1:17
.=
((len ((I | (n + m)) | n)) + (len (I /^ (n + m)))) + (len ((I | (n + m)) /^ n))
by AFINSQ_1:17
.=
((len ((I | (n + m)) | n)) + (len ((I | (n + m)) /^ n))) + (len (I /^ (n + m)))
.=
(len (I | (n + m))) + (len (I /^ (n + m)))
by A4, AFINSQ_1:17
.=
len I
by A3, AFINSQ_1:17
;
then reconsider III = (((I | (n + m)) | n) ^ (I /^ (n + m))) ^ ((I | (n + m)) /^ n) as Function of ((n + k) + m),((n + k) + m) by A12, FUNCT_2:1;
III is onto
by A12;
then reconsider III = III as Permutation of ((n + k) + m) by A11;
take T = P1 permuted_by (III "); ( rng T c= (rng p) \/ {(0. L)} & ( for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (T,XanyY) ) )
thus
rng T c= (rng p) \/ {(0. L)}
by A1, Th26; for XY being Function of (n + m),L
for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (T,XanyY)
let XY be Function of (n + m),L; for XanyY being Function of ((n + k) + m),L st XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) holds
eval (p,XY) = eval (T,XanyY)
let XanyY be Function of ((n + k) + m),L; ( XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) implies eval (p,XY) = eval (T,XanyY) )
assume A13:
( XY | n = XanyY | n & (@ XY) /^ n = (@ XanyY) /^ (n + k) )
; eval (p,XY) = eval (T,XanyY)
A14:
( len (@ XY) = n + m & len (@ XanyY) = (n + k) + m )
by FUNCT_2:def 1;
then A15: len ((@ XY) /^ n) =
(n + m) -' n
by AFINSQ_2:def 2
.=
m
by NAT_D:34
;
A16: len ((@ XanyY) /^ (n + k)) =
((n + k) + m) -' (n + k)
by A14, AFINSQ_2:def 2
.=
m
by NAT_D:34
;
len ((@ XanyY) | (n + k)) = n + k
by A14, AFINSQ_1:54, NAT_1:11;
then A17: len (((@ XanyY) | (n + k)) /^ n) =
(n + k) -' n
by AFINSQ_2:def 2
.=
k
by NAT_D:34
;
then A18:
len ((@ XY) ^ (((@ XanyY) | (n + k)) /^ n)) = (n + m) + k
by A14, AFINSQ_1:17;
rng ((@ XY) ^ (((@ XanyY) | (n + k)) /^ n)) c= the carrier of L
by RELAT_1:def 19;
then reconsider R = (@ XY) ^ (((@ XanyY) | (n + k)) /^ n) as Function of ((n + m) + k),L by A18, FUNCT_2:2;
reconsider r = R as Function of ((n + k) + m),L ;
R | (n + m) =
(@ XY) | (n + m)
by AFINSQ_1:58, A14
.=
@ XY
;
then A19:
eval (p,XY) = eval (P,R)
by A2;
(III ") " = III
by FUNCT_1:43;
then A20:
eval (P1,r) = eval (T,(r * III))
by Th25;
A21:
( dom (@ (r * III)) = (n + k) + m & (n + k) + m = dom (@ XanyY) )
by FUNCT_2:def 1;
n + m <= (n + m) + k
by NAT_1:11;
then
n + m <= len I
;
then A22:
( len (I | (n + m)) = n + m & len (I /^ (n + m)) = ((n + m) + k) -' (n + m) )
by AFINSQ_1:54, AFINSQ_2:def 2;
then A23:
len (I /^ (n + m)) = k
by NAT_D:34;
A24:
n <= n + m
by NAT_1:11;
A25:
( len ((I | (n + m)) | n) = n & len ((I | (n + m)) /^ n) = (n + m) -' n )
by A22, NAT_1:11, AFINSQ_1:54, AFINSQ_2:def 2;
then A26:
len ((I | (n + m)) /^ n) = m
by NAT_D:34;
A27:
len (((I | (n + m)) | n) ^ (I /^ (n + m))) = n + k
by A23, A25, AFINSQ_1:17;
for k being Nat st k in dom (@ XanyY) holds
(@ (r * III)) . k = (@ XanyY) . k
proof
let w be
Nat;
( w in dom (@ XanyY) implies (@ (r * III)) . w = (@ XanyY) . w )
assume A28:
w in dom (@ XanyY)
;
(@ (r * III)) . w = (@ XanyY) . w
per cases
( w < n or ( n + k > w & w >= n ) or w >= n + k )
;
suppose A29:
w < n
;
(@ (r * III)) . w = (@ XanyY) . wthen A30:
(
w in dom ((I | (n + m)) | n) &
dom ((I | (n + m)) | n) c= dom (((I | (n + m)) | n) ^ (I /^ (n + m))) )
by A25, AFINSQ_1:66, AFINSQ_1:21;
w < n + m
by A29, A24, XXREAL_0:2;
then A31:
w in Segm (n + m)
by NAT_1:44;
A32:
III . w =
(((I | (n + m)) | n) ^ (I /^ (n + m))) . w
by AFINSQ_1:def 3, A30
.=
((I | (n + m)) | n) . w
by A30, AFINSQ_1:def 3
.=
(I | (n + m)) . w
by A29, A25, AFINSQ_1:66, FUNCT_1:47
.=
I . w
by A31, FUNCT_1:49
.=
w
by A21, A28, FUNCT_1:17
;
w + 0 < n + m
by A29, XREAL_1:8;
then
w in dom (@ XY)
by A14, AFINSQ_1:66;
then r . w =
(@ XY) . w
by AFINSQ_1:def 3
.=
((@ XY) | n) . w
by A29, A25, AFINSQ_1:66, FUNCT_1:49
.=
XanyY . w
by A13, A29, A25, AFINSQ_1:66, FUNCT_1:49
;
hence
(@ (r * III)) . w = (@ XanyY) . w
by A32, A28, FUNCT_1:12, A21;
verum end; suppose A33:
(
n + k > w &
w >= n )
;
(@ (r * III)) . w = (@ XanyY) . wthen reconsider wn =
w - n as
Nat by NAT_1:21;
n + k > n + wn
by A33;
then A34:
wn in Segm k
by NAT_1:44, XREAL_1:6;
A35:
w in Segm (n + k)
by A33, NAT_1:44;
(n + m) + wn = m + w
;
then
(n + m) + wn < m + (n + k)
by A33, XREAL_1:6;
then A36:
(n + m) + wn in Segm ((n + m) + k)
by NAT_1:44;
w in dom (((I | (n + m)) | n) ^ (I /^ (n + m)))
by A33, A27, AFINSQ_1:66;
then A37:
III . w =
(((I | (n + m)) | n) ^ (I /^ (n + m))) . w
by AFINSQ_1:def 3
.=
(I /^ (n + m)) . wn
by A33, AFINSQ_1:18, A23, A25
.=
I . ((n + m) + wn)
by A23, A34, AFINSQ_2:def 2
.=
(n + m) + wn
by A36, FUNCT_1:17
;
r . ((n + m) + wn) =
(((@ XanyY) | (n + k)) /^ n) . wn
by A14, A17, A34, AFINSQ_1:def 3
.=
((@ XanyY) | (n + k)) . (wn + n)
by A17, A34, AFINSQ_2:def 2
.=
(@ XanyY) . w
by A35, FUNCT_1:49
;
hence
(@ (r * III)) . w = (@ XanyY) . w
by A37, A28, FUNCT_1:12, A21;
verum end; suppose
w >= n + k
;
(@ (r * III)) . w = (@ XanyY) . wthen reconsider wnk =
w - (n + k) as
Nat by NAT_1:21;
A38:
(n + k) + m > (n + k) + wnk
by A28, A14, AFINSQ_1:66;
then A39:
m > wnk
by XREAL_1:6;
A40:
wnk in Segm m
by NAT_1:44, A38, XREAL_1:6;
then A41:
wnk in dom ((I | (n + m)) /^ n)
by A25, NAT_D:34;
wnk + n < m + n
by A39, XREAL_1:6;
then
(wnk + n) + 0 < (m + n) + k
by XREAL_1:8;
then A42:
(
wnk + n in Segm ((n + k) + m) &
wnk + n in Segm (m + n) )
by A39, XREAL_1:6, NAT_1:44;
A43:
III . ((n + k) + wnk) =
((I | (n + m)) /^ n) . wnk
by A40, A26, A27, AFINSQ_1:def 3
.=
(I | (n + m)) . (n + wnk)
by A41, AFINSQ_2:def 2
.=
I . (n + wnk)
by A42, FUNCT_1:49
.=
n + wnk
by A42, FUNCT_1:17
;
r . (n + wnk) =
(@ XY) . (n + wnk)
by A14, A42, AFINSQ_1:def 3
.=
((@ XY) /^ n) . wnk
by A40, A15, AFINSQ_2:def 2
.=
(@ XanyY) . ((n + k) + wnk)
by A13, A16, A40, AFINSQ_2:def 2
;
hence
(@ (r * III)) . w = (@ XanyY) . w
by A43, A28, FUNCT_1:12, A21;
verum end;
end;
hence
eval (p,XY) = eval (T,XanyY)
by A20, A19, A21, AFINSQ_1:8; verum