let X be Ordinal; :: thesis: for L being non empty ZeroStr
for s being Series of X,L
for perm being Permutation of X holds vars (s permuted_by perm) c= perm .: (vars s)
let L be non empty ZeroStr ; :: thesis: for s being Series of X,L
for perm being Permutation of X holds vars (s permuted_by perm) c= perm .: (vars s)
let s be Series of X,L; :: thesis: for perm being Permutation of X holds vars (s permuted_by perm) c= perm .: (vars s)
let perm be Permutation of X; :: thesis: vars (s permuted_by perm) c= perm .: (vars s)
set S = s permuted_by perm;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars (s permuted_by perm) or x in perm .: (vars s) )
assume x in vars (s permuted_by perm) ; :: thesis: x in perm .: (vars s)
then consider b being bag of X such that
A1: ( b in Support (s permuted_by perm) & b . x <> 0 ) by Def5;
A2: b * perm in Support s by A1, HILB10_2:21;
reconsider B = b * perm as bag of X ;
A3: ( x in dom b & dom b = X ) by A1, FUNCT_1:def 2, PARTFUN1:def 2;
( rng perm = X & X = dom perm ) by FUNCT_2:def 3, FUNCT_2:52;
then consider y being object such that
A4: ( y in dom perm & perm . y = x ) by A3, FUNCT_1:def 3;
y in dom (b * perm) by A4, A3, FUNCT_1:11;
then B . y <> 0 by A1, A4, FUNCT_1:12;
then y in vars s by A2, Def5;
hence x in perm .: (vars s) by A4, FUNCT_1:def 6; :: thesis: verum