let L be Field; for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
let p be non-zero Polynomial of L; for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
let a be Element of L; for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
let b be non zero Element of L; for E being Enumeration of Roots (<%a,b%> *' p)
for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
set q = <%a,b%>;
set B = BRoots (<%a,b%> *' p);
let E be Enumeration of Roots (<%a,b%> *' p); for P being Permutation of (dom E) holds ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
let P be Permutation of (dom E); ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
len E = len ((BRoots (<%a,b%> *' p)) (++) E)
by Def1;
then A1:
dom E = dom ((BRoots (<%a,b%> *' p)) (++) E)
by FINSEQ_3:29;
then reconsider P1 = P as Permutation of (dom ((BRoots (<%a,b%> *' p)) (++) E)) ;
((BRoots (<%a,b%> *' p)) (++) E) * P1 = (BRoots (<%a,b%> *' p)) (++) (E * P)
proof
A2:
len (E * P) = len ((BRoots (<%a,b%> *' p)) (++) (E * P))
by Def1;
A3:
rng P = dom E
by FUNCT_2:def 3;
then A4:
dom (((BRoots (<%a,b%> *' p)) (++) E) * P1) = dom P1
by A1, RELAT_1:27;
A5:
dom P1 = dom (E * P)
by A3, RELAT_1:27;
hence A6:
len (((BRoots (<%a,b%> *' p)) (++) E) * P1) = len ((BRoots (<%a,b%> *' p)) (++) (E * P))
by A2, A4, FINSEQ_3:29;
FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len (((BRoots (<%a,b%> *' p)) (++) E) * P1) or (((BRoots (<%a,b%> *' p)) (++) E) * P1) . b1 = ((BRoots (<%a,b%> *' p)) (++) (E * P)) . b1 )
let n be
Nat;
( not 1 <= n or not n <= len (((BRoots (<%a,b%> *' p)) (++) E) * P1) or (((BRoots (<%a,b%> *' p)) (++) E) * P1) . n = ((BRoots (<%a,b%> *' p)) (++) (E * P)) . n )
assume that A7:
1
<= n
and A8:
n <= len (((BRoots (<%a,b%> *' p)) (++) E) * P1)
;
(((BRoots (<%a,b%> *' p)) (++) E) * P1) . n = ((BRoots (<%a,b%> *' p)) (++) (E * P)) . n
A9:
n in dom (((BRoots (<%a,b%> *' p)) (++) E) * P1)
by A7, A8, FINSEQ_3:25;
A10:
((BRoots (<%a,b%> *' p)) * E) . (P1 . n) =
(((BRoots (<%a,b%> *' p)) * E) * P1) . n
by A4, A7, A8, FINSEQ_3:25, FUNCT_1:13
.=
((BRoots (<%a,b%> *' p)) * (E * P)) . n
by RELAT_1:36
;
A11:
P1 . n in rng P1
by A4, A9, FUNCT_1:def 3;
then A12:
( 1
<= P1 . n &
P1 . n <= len ((BRoots (<%a,b%> *' p)) (++) E) )
by FINSEQ_3:25;
A13:
E /. (P1 . n) =
E . (P1 . n)
by A3, A11, PARTFUN1:def 6
.=
(E * P1) . n
by A4, A7, A8, FINSEQ_3:25, FUNCT_1:13
.=
(E * P) /. n
by A4, A5, A7, A8, FINSEQ_3:25, PARTFUN1:def 6
;
thus (((BRoots (<%a,b%> *' p)) (++) E) * P1) . n =
((BRoots (<%a,b%> *' p)) (++) E) . (P1 . n)
by A4, A7, A8, FINSEQ_3:25, FUNCT_1:13
.=
(((BRoots (<%a,b%> *' p)) * E) . (P1 . n)) * (E /. (P1 . n))
by A12, Def1
.=
((BRoots (<%a,b%> *' p)) (++) (E * P)) . n
by A6, A7, A8, A10, A13, Def1
;
verum
end;
hence
((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P)
; verum