consider h being Function of [:F₁(),NAT:],F₂() such that
a1: for a being Element of F₁() holds
( h . (a,0) = F₃() . a & ( for n being Nat holds h . (a,(n + 1)) = F₄((h . (a,n)),a,n) ) ) from DBLSEQ_2:sch 1();
take g = ~ h; :: thesis: for a being Element of F₁() holds
( g . (0,a) = F₃() . a & ( for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n) ) )

hereby :: thesis: verum

let a be Element of F₁(); :: thesis: ( g . (0,a) = F₃() . a & ( for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n) ) )
thus g . (0,a) = h . (a,0) by FUNCT_4:def 8
.= F₃() . a by a1 ; :: thesis: for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n)
thus for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n) :: thesis: verum

proof

let n be Nat; :: thesis: g . ((n + 1),a) = F₄((g . (n,a)),a,n)
a2: n in NAT by ORDINAL1:def 12;
g . ((n + 1),a) = h . (a,(n + 1)) by FUNCT_4:def 8;
then g . ((n + 1),a) = F₄((h . (a,n)),a,n) by a1;
hence g . ((n + 1),a) = F₄((g . (n,a)),a,n) by a2, FUNCT_4:def 8; :: thesis: verum

end;

end;