consider h being Function of [:F₁(),NAT:],REAL 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 2();
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;