let p, q be FinSequence; :: thesis: for f being Permutation of dom p st q = p * f holds
len q = len p
Seg (len p) = dom p by FINSEQ_1:def 3;
hence for f being Permutation of dom p st q = p * f holds
len q = len p by Th47; :: thesis: verum