let i be natural Number ; :: 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 Th39; :: thesis: verum