deffunc H₁( Nat) -> Element of REAL = (MemberFunc ((X . $1),A)) . x;
ex z being FinSequence of REAL st
( len z = len X & ( for j being Nat st j in dom z holds
z . j = H₁(j) ) ) from FINSEQ_2:sch 1();
then consider z being FinSequence of REAL such that
A1: len z = len X and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) ;
take z ; :: thesis: ( dom z = dom X & ( for n being Nat st n in dom X holds
z . n = (MemberFunc ((X . n),A)) . x ) )
thus dom z = Seg (len z) by FINSEQ_1:def 3
.= dom X by A1, FINSEQ_1:def 3 ; :: thesis: for n being Nat st n in dom X holds
z . n = (MemberFunc ((X . n),A)) . x
let n be Nat; :: thesis: ( n in dom X implies z . n = (MemberFunc ((X . n),A)) . x )
assume n in dom X ; :: thesis: z . n = (MemberFunc ((X . n),A)) . x
then A3: n in Seg (len X) by FINSEQ_1:def 3;
dom z = Seg (len X) by A1, FINSEQ_1:def 3;
hence z . n = (MemberFunc ((X . n),A)) . x by A2, A3; :: thesis: verum