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 in Support (s permuted_by perm) iff b * perm 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 in Support (s permuted_by perm) iff b * perm 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 in Support (s permuted_by perm) iff b * perm in Support s )
let s be Series of O,L; :: thesis: for b being bag of O holds
( b in Support (s permuted_by perm) iff b * perm in Support s )
let b be bag of O; :: thesis: ( b in Support (s permuted_by perm) iff b * perm 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: (s permuted_by perm) . b = s . (b * perm) by Def4;
thus ( b in Support (s permuted_by perm) implies b * perm in Support s ) :: thesis: ( b * perm in Support s implies b in Support (s permuted_by perm) )

proof

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

end;

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