let L be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ((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; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (((BRoots (<%a,b%> *' p)) (++) E) * P1) or (((BRoots (<%a,b%> *' p)) (++) E) * P1) . b₁ = ((BRoots (<%a,b%> *' p)) (++) (E * P)) . b₁ )
let n be Nat; :: thesis: ( 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) ; :: thesis: (((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 ; :: thesis: verum

end;

hence ((BRoots (<%a,b%> *' p)) (++) E) * P = (BRoots (<%a,b%> *' p)) (++) (E * P) ; :: thesis: verum