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 10(A6, A1, A2, A5, A3, A4); :: thesis: verum