let n be Element of NAT ; :: thesis: for K being Field
for p being Element of Permutations n
for f, g being FinSequence of K st n >= 1 & len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let K be Field; :: thesis: for p being Element of Permutations n
for f, g being FinSequence of K st n >= 1 & 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 n >= 1 & len f = n & g = f * p holds
f,g are_fiberwise_equipotent
let f, g be FinSequence of K; :: thesis: ( n >= 1 & len f = n & g = f * p implies f,g are_fiberwise_equipotent )
assume A1: ( n >= 1 & len f = n & g = f * p ) ; :: thesis: f,g are_fiberwise_equipotent
A3: p is Permutation of (Seg n) by MATRIX_2:def 11;
reconsider fp = p as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
rng fp = Seg n by A3, FUNCT_2:def 3;
then rng p c= dom f by A1, FINSEQ_1:def 3;
then A4: dom (f * p) = dom fp by RELAT_1:46;
A5: rng p = Seg n by A3, FUNCT_2:def 3;
dom f = Seg n by A1, FINSEQ_1:def 3;
hence f,g are_fiberwise_equipotent by A1, A4, A5, CLASSES1:85; :: thesis: verum