consider h being Function of [:F1(),NAT:],REAL such that
a1: for a being Element of F1() holds
( h . (a,0) = F2() . a & ( for n being Nat holds h . (a,(n + 1)) = F3((h . (a,n)),a,n) ) ) from DBLSEQ_2:sch 2();
 take g = ~ h; :: thesis: for a being Element of F1() holds
( g . (0,a) = F2() . a & ( for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n) ) )
hereby :: thesis: verum
let a be Element of F1(); :: thesis: ( g . (0,a) = F2() . a & ( for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n) ) )
thus g . (0,a) = h . (a,0) by FUNCT_4:def 8
.= F2() . a by a1 ; :: thesis: for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n)
thus for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n) :: thesis: verum
proof
let n be Nat; :: thesis: g . ((n + 1),a) = F3((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) = F3((h . (a,n)),a,n) by a1;
hence g . ((n + 1),a) = F3((g . (n,a)),a,n) by a2, FUNCT_4:def 8; :: thesis: verum
end;
end;