let f be Function; :: thesis: ( ex k being Nat st dom f c= Seg k implies ex p being FinSequence st f c= p )
given k being Nat such that A1: dom f c= Seg k ; :: thesis: ex p being FinSequence st f c= p
deffunc H₁( object ) -> set = f . $1;
consider g being Function such that
A2: ( dom g = Seg k & ( for x being object st x in Seg k holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider g = g as FinSequence by A2, Def2;
take g ; :: thesis: f c= g
let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in f or [y,z] in g )
assume A3: [y,z] in f ; :: thesis: [y,z] in g
then A4: y in dom f by XTUPLE_0:def 12;
reconsider z = z as set by TARSKI:1;
A5: f . y = z by A3, FUNCT_1:def 2, A4;
[y,(g . y)] in g by A1, A2, A4, FUNCT_1:1;
hence [y,z] in g by A1, A2, A4, A5; :: thesis: verum