let O be Ordinal; :: thesis: for L being non empty ZeroStr
for perm being Permutation of O
for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))
let L be non empty ZeroStr ; :: thesis: for perm being Permutation of O
for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))
let perm be Permutation of O; :: thesis: for s being Series of O,L holds card (Support s) = card (Support (s permuted_by perm))
let s be Series of O,L; :: thesis: card (Support s) = card (Support (s permuted_by perm))
set P = s permuted_by perm;
defpred S₁[ bag of O, bag of O] means $2 = $1 * perm;
A1: for x being Element of Bags O ex y being Element of Bags O st S₁[x,y]

proof

let x be Element of Bags O; :: thesis: ex y being Element of Bags O st S₁[x,y]
x * perm in Bags O by PRE_POLY:def 12;
hence ex y being Element of Bags O st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of (Bags O),(Bags O) such that
A2: for x being Element of Bags O holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
A3: dom f = Bags O by FUNCT_2:52;
( rng perm = O & O = dom perm ) by FUNCT_2:52, FUNCT_2:def 3;
then A4: ( perm * (perm ") = id O & id O = (perm ") * perm ) by FUNCT_1:39;
A5: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A6: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of Bags O by A6;
A7: ( f . x1 = x1 * perm & f . x2 = x2 * perm ) by A2;
A8: ( dom x1 = O & O = dom x2 ) by PARTFUN1:def 2;
A9: (x1 * perm) * (perm ") = x1 * (id O) by A4, RELAT_1:36
.= x1 by A8, RELAT_1:51 ;
(x2 * perm) * (perm ") = x2 * (id O) by A4, RELAT_1:36
.= x2 by A8, RELAT_1:51 ;
hence x1 = x2 by A6, A7, A9; :: thesis: verum

end;

A10: f .: (Support (s permuted_by perm)) c= Support s

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Support (s permuted_by perm)) or y in Support s )
assume A11: y in f .: (Support (s permuted_by perm)) ; :: thesis: y in Support s
consider x being object such that
A12: ( x in dom f & x in Support (s permuted_by perm) & f . x = y ) by A11, FUNCT_1:def 6;
reconsider x = x as Element of Bags O by A12;
( f . x = x * perm & x * perm in Support s ) by A2, Th21, A12;
hence y in Support s by A12; :: thesis: verum

end;

Support s c= f .: (Support (s permuted_by perm))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support s or y in f .: (Support (s permuted_by perm)) )
assume A13: y in Support s ; :: thesis: y in f .: (Support (s permuted_by perm))
reconsider y = y as Element of Bags O by A13;
A14: y * (perm ") in Support (s permuted_by perm) by A13, Th22;
A15: dom y = O by PARTFUN1:def 2;
y * (perm ") in Bags O by PRE_POLY:def 12;
then f . (y * (perm ")) = (y * (perm ")) * perm by A2
.= y * (id O) by A4, RELAT_1:36
.= y by A15, RELAT_1:51 ;
hence y in f .: (Support (s permuted_by perm)) by A3, FUNCT_1:def 6, A14; :: thesis: verum

end;

then f .: (Support (s permuted_by perm)) = Support s by A10, XBOOLE_0:def 10;
hence card (Support s) = card (Support (s permuted_by perm)) by CARD_1:5, A5, A3, CARD_1:33; :: thesis: verum