( dom rf = dom (sqrt rf) & ex n being Nat st dom rf = Seg n ) by FINSEQ_1:def 2, PARTFUN3:def 5;
hence sqrt rf is FinSequence-like ; :: thesis: verum