let f be FinSequence; :: thesis: for h being Function st dom h = dom f holds
h is FinSequence
let h be Function; :: thesis: ( dom h = dom f implies h is FinSequence )
assume A1: dom h = dom f ; :: thesis: h is FinSequence
h is FinSequence-like

proof

take len f ; :: according to FINSEQ_1:def 2 :: thesis: dom h = Seg (len f)
thus dom h = Seg (len f) by A1, FINSEQ_1:def 3; :: thesis: verum

end;

hence h is FinSequence ; :: thesis: verum