deffunc H₁( Nat) -> Element of K16(K17(X,Y)) = (F . $1) | D;
ex G being Functional_Sequence of X,Y st
for n being Nat holds G . n = H₁(n) from SEQFUNC:sch 1();
hence ex b₁ being Functional_Sequence of X,Y st
for n being Nat holds b₁ . n = (F . n) | D ; :: thesis: verum