let X be set ; :: thesis: for S being with_evenly_repeated_values-member set st ( for x being Element of S st x in S holds
dom x = X ) holds
for p being Permutation of X holds { (s * p) where s is FinSequence of NAT : s in S } is with_evenly_repeated_values-member
let S be with_evenly_repeated_values-member set ; :: thesis: ( ( for x being Element of S st x in S holds
dom x = X ) implies for p being Permutation of X holds { (s * p) where s is FinSequence of NAT : s in S } is with_evenly_repeated_values-member )
assume A1: for x being Element of S st x in S holds
dom x = X ; :: thesis: for p being Permutation of X holds { (s * p) where s is FinSequence of NAT : s in S } is with_evenly_repeated_values-member
let p be Permutation of X; :: thesis: { (s * p) where s is FinSequence of NAT : s in S } is with_evenly_repeated_values-member
let y be object ; :: according to HILB10_7:def 7 :: thesis: ( y in { (s * p) where s is FinSequence of NAT : s in S } implies y is finite with_evenly_repeated_values Function )
assume y in { (s * p) where s is FinSequence of NAT : s in S } ; :: thesis: y is finite with_evenly_repeated_values Function
then consider s being FinSequence of NAT such that
A2: ( y = s * p & s in S ) ;
dom s = X by A2, A1;
then reconsider pp = p as Permutation of (dom s) ;
s * pp is with_evenly_repeated_values by A2, Th44;
hence y is finite with_evenly_repeated_values Function by A2; :: thesis: verum