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