deffunc H_{1}( 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_{1}(n)
from SEQFUNC:sch 1();

hence ex b_{1} being Functional_Sequence of X,Y st

for n being Nat holds b_{1} . n = (F . n) | D
; :: thesis: verum

ex G being Functional_Sequence of X,Y st

for n being Nat holds G . n = H

hence ex b

for n being Nat holds b