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