consider f being Function such that
A1: ( dom f = Seg F₁() & ( for x being object st x in Seg F₁() holds
f . x = F₂(x) ) ) from FUNCT_1:sch 3();
A2: F₁() in NAT by ORDINAL1:def 12;
reconsider p = f as FinSequence by A1, Def2;
take p ; :: thesis: ( len p = F₁() & ( for k being Nat st k in dom p holds
p . k = F₂(k) ) )
thus ( len p = F₁() & ( for k being Nat st k in dom p holds
p . k = F₂(k) ) ) by A1, A2, Def3; :: thesis: verum