let O be Ordinal; :: thesis: for L being non empty ZeroStr
for perm being Permutation of O
for s being Series of O,L
for b being bag of O holds
( b * (perm ") in Support (s permuted_by perm) iff b in Support s )
let L be non empty ZeroStr ; :: thesis: for perm being Permutation of O
for s being Series of O,L
for b being bag of O holds
( b * (perm ") in Support (s permuted_by perm) iff b in Support s )
let perm be Permutation of O; :: thesis: for s being Series of O,L
for b being bag of O holds
( b * (perm ") in Support (s permuted_by perm) iff b in Support s )
let s be Series of O,L; :: thesis: for b being bag of O holds
( b * (perm ") in Support (s permuted_by perm) iff b in Support s )
let b be bag of O; :: thesis: ( b * (perm ") in Support (s permuted_by perm) iff b in Support s )
set P = s permuted_by perm;
A1: ( dom (s permuted_by perm) = Bags O & Bags O = dom s ) by FUNCT_2:def 1;
A2: dom b = O by PARTFUN1:def 2;
dom perm = O by FUNCT_2:52;
then (perm ") * perm = id O by FUNCT_1:39;
then (b * (perm ")) * perm = b * (id O) by RELAT_1:36
.= b by A2, RELAT_1:51 ;
then A3: (s permuted_by perm) . (b * (perm ")) = s . b by Def4;
thus ( b * (perm ") in Support (s permuted_by perm) implies b in Support s ) :: thesis: ( b in Support s implies b * (perm ") in Support (s permuted_by perm) )

proof

assume b * (perm ") in Support (s permuted_by perm) ; :: thesis: b in Support s
then A4: (s permuted_by perm) . (b * (perm ")) <> 0. L by POLYNOM1:def 3;
b in Bags O by PRE_POLY:def 12;
hence b in Support s by A4, A1, A3, POLYNOM1:def 3; :: thesis: verum

end;

assume b in Support s ; :: thesis: b * (perm ") in Support (s permuted_by perm)
then A5: s . b <> 0. L by POLYNOM1:def 3;
b * (perm ") in Bags O by PRE_POLY:def 12;
hence b * (perm ") in Support (s permuted_by perm) by A5, A1, A3, POLYNOM1:def 3; :: thesis: verum