deffunc H1( Nat) -> Element of the carrier of R = ((n choose ($1 -' 1)) * ((D |^ ((n + 1) -' $1)) . x)) * ((D |^ ($1 -' 1)) . y);
consider z being FinSequence such that
A1: ( len z = n + 1 & ( for k being Nat st k in dom z holds
z . k = H1(k) ) ) from FINSEQ_1:sch 2();
 take z ; :: thesis: ( z is Element of K10(K11(NAT, the carrier of R)) & z is FinSequence of the carrier of R & len z = n + 1 & ( for i being Nat st i in dom z holds
z . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) )
z is FinSequence of R
proof
A2: for p being object st p in rng z holds
p in the carrier of R
proof
let p be object ; :: thesis: ( p in rng z implies p in the carrier of R )
assume p in rng z ; :: thesis: p in the carrier of R
then consider i being object such that
A3: i in dom z and
A4: p = z . i by FUNCT_1:def 3;
reconsider i = i as Nat by A3;
z . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) by A1, A3;
hence p in the carrier of R by A4; :: thesis: verum
end;
rng z c= the carrier of R by A2;
hence z is FinSequence of R by FINSEQ_1:def 4; :: thesis: verum
end;
hence ( z is Element of K10(K11(NAT, the carrier of R)) & z is FinSequence of the carrier of R & len z = n + 1 & ( for i being Nat st i in dom z holds
z . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) ) by A1; :: thesis: verum