A5: dom F₇() = NAT by FUNCT_2:def 1;
A6: dom F₆() = NAT by FUNCT_2:def 1;
thus F₆() = F₇() from RECDEF_2:sch 14(A6, A1, A2, A5, A3, A4); :: thesis: verum