let i be Nat; :: thesis: for p, q being FinSequence
for f being Permutation of Seg i st i <= len p & q = p * f holds
len q = i
let p, q be FinSequence; :: thesis: for f being Permutation of Seg i st i <= len p & q = p * f holds
len q = i
let f be Permutation of Seg i; :: thesis: ( i <= len p & q = p * f implies len q = i )
rng f = Seg i by FUNCT_2:def 3;
hence ( i <= len p & q = p * f implies len q = i ) by Th45; :: thesis: verum