let O be Ordinal; :: thesis: for L being non empty ZeroStr
for s being Series of O,L
for perm being Permutation of O holds rng (s permuted_by perm) = rng s
let L be non empty ZeroStr ; :: thesis: for s being Series of O,L
for perm being Permutation of O holds rng (s permuted_by perm) = rng s
let s be Series of O,L; :: thesis: for perm being Permutation of O holds rng (s permuted_by perm) = rng s
let perm be Permutation of O; :: thesis: rng (s permuted_by perm) = rng s
set P = s permuted_by perm;
A1: ( dom (s permuted_by perm) = Bags O & dom s = Bags O ) by FUNCT_2:def 1;
thus rng (s permuted_by perm) c= rng s :: according to XBOOLE_0:def 10 :: thesis: rng s c= rng (s permuted_by perm)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (s permuted_by perm) or y in rng s )
assume y in rng (s permuted_by perm) ; :: thesis: y in rng s
then consider x being object such that
A2: ( x in dom (s permuted_by perm) & (s permuted_by perm) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags O by A2;
A3: x * perm in dom s by A1, PRE_POLY:def 12;
s . (x * perm) = (s permuted_by perm) . x by Def4;
hence y in rng s by A3, FUNCT_1:def 3, A2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in rng (s permuted_by perm) )
assume y in rng s ; :: thesis: y in rng (s permuted_by perm)
then consider x being object such that
A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags O by A4;
A5: dom x = O by PARTFUN1:def 2;
dom perm = O by FUNCT_2:52;
then (perm ") * perm = id O by FUNCT_1:39;
then (x * (perm ")) * perm = x * (id O) by RELAT_1:36
.= x by A5, RELAT_1:51 ;
then A6: (s permuted_by perm) . (x * (perm ")) = s . x by Def4;
x * (perm ") in dom (s permuted_by perm) by A1, PRE_POLY:def 12;
hence y in rng (s permuted_by perm) by A4, A6, FUNCT_1:def 3; :: thesis: verum