let m be Nat; :: thesis: for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))
let F be finite set ; :: thesis: for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))
let E be Enumeration of F; :: thesis: for p being Permutation of (dom E)
for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))
let p be Permutation of (dom E); :: thesis: for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))
let s be FinSequence; :: thesis: ( s in doms (m,(card F)) implies s * p in doms (m,(card F)) )
assume A1: s in doms (m,(card F)) ; :: thesis: s * p in doms (m,(card F))
reconsider s1 = s as Element of doms (m,(card F)) by A1;
reconsider Ep = E * p as Enumeration of F by Th109;
A2: ( len s = card F & card F = card E ) by Th121, A1, CARD_1:def 7;
then A3: dom E = dom s by FINSEQ_3:30;
A4: ( dom p = dom E & dom E = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
then A5: ( dom (s * p) = dom s & dom s = Seg (len s) ) by A3, RELAT_1:27, FINSEQ_1:def 3;
reconsider sp = s * p as FinSequence by A3;
A6: len sp = len s by A5, FINSEQ_3:29;
A7: rng s1 c= Seg m ;
rng sp = rng s by A3, A4, RELAT_1:28;
then sp is FinSequence of Seg m by A7, FINSEQ_1:def 4;
then sp in (Seg m) * by FINSEQ_1:def 11;
hence s * p in doms (m,(card F)) by A2, A6; :: thesis: verum