let n be Nat; :: thesis: for K being commutative Ring
for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let K be commutative Ring; :: thesis: for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let p be Element of Permutations n; :: thesis: for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let f, g be FinSequence of K; :: thesis: ( len f = n & g = f * p implies f,g are_fiberwise_equipotent )
assume that
A1: len f = n and
A2: g = f * p ; :: thesis: f,g are_fiberwise_equipotent
reconsider fp = p as Function of (Seg n),(Seg n) by MATRIX_1:def 12;
A3: p is Permutation of (Seg n) by MATRIX_1:def 12;
then A4: rng p = Seg n by FUNCT_2:def 3;
rng fp = Seg n by A3, FUNCT_2:def 3;
then rng p c= dom f by A1, FINSEQ_1:def 3;
then A5: dom (f * p) = dom fp by RELAT_1:27;
dom f = Seg n by A1, FINSEQ_1:def 3;
hence f,g are_fiberwise_equipotent by A2, A5, A4, CLASSES1:77; :: thesis: verum