consider g being FinSequence of F₁() such that
A1: ( len g = F₂() & ( for n being Nat st n in dom g holds
g . n = F₃(n) ) ) from FINSEQ_2:sch 1();
take g ; :: thesis: ( len g = F₂() & ( for n being Nat st n in dom g holds
g /. n = F₃(n) ) )
thus len g = F₂() by A1; :: thesis: for n being Nat st n in dom g holds
g /. n = F₃(n)
let n be Nat; :: thesis: ( n in dom g implies g /. n = F₃(n) )
assume A2: n in dom g ; :: thesis: g /. n = F₃(n)
then g . n = F₃(n) by A1;
hence g /. n = F₃(n) by A2, PARTFUN1:def 6; :: thesis: verum