now

per cases ( len F = 0 or len F <> 0 ) ;

suppose len F = 0 ; :: thesis: ( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & b₁ = f . ((len F) - 1) ) ) )

hence ( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & b₁ = f . ((len F) - 1) ) ) ) by A1; :: thesis: verum

end;

suppose A2: len F <> 0 ; :: thesis: ( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & b₁ = f . ((len F) - 1) ) ) )

defpred S₁[ Element of NAT ] means for F being XFinSequence of st len F = $1 & len F <> 0 holds
ex d being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) );
A3: S₁[ 0 ] ;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let F be XFinSequence of ; :: thesis: ( len F = k + 1 & len F <> 0 implies ex d being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) ) )
assume A6: ( len F = k + 1 & len F <> 0 ) ; :: thesis: ex d being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) )
reconsider G = F | k as XFinSequence of by AFINSQ_1:16;
B7: k < k + 1 by NAT_1:13;
then A7: len G = k by A6, AFINSQ_1:14;

now

per cases ( len G = 0 or len G <> 0 ) ;

suppose A8: len G = 0 ; :: thesis: ex d being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) )

then 0 in dom F by A6, A7, CARD_1:87, TARSKI:def 1;
then A9: F . 0 in rng F by FUNCT_1:def 5;
rng F c= D by RELAT_1:def 19;
then reconsider f = NAT --> (F . 0 ) as Function of NAT ,D by A9, FUNCOP_1:57;
take d = f . 0 ; :: thesis: ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) )
take f = f; :: thesis: ( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) )
thus f . 0 = F . 0 by FUNCOP_1:13; :: thesis: ( ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) )
thus for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) by A6, A7, A8, NAT_1:14; :: thesis: d = f . ((len F) - 1)
k < k + 1 by NAT_1:13;
hence d = f . ((len F) - 1) by A6, A8, AFINSQ_1:14; :: thesis: verum

end;

suppose A10: len G <> 0 ; :: thesis: ex a being Element of D ex h being Function of NAT ,D st
( h . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
h . (n + 1) = b . (h . n),(F . (n + 1)) ) & a = h . ((len F) - 1) )

then consider d being Element of D, f being Function of NAT ,D such that
A11: f . 0 = G . 0 and
A12: for n being Element of NAT st n + 1 < len G holds
f . (n + 1) = b . (f . n),(G . (n + 1)) and
A13: d = f . ((len G) - 1) by A5, B7, A6, AFINSQ_1:14;
( k < len F & len F = dom F ) by A6, NAT_1:13;
then k in dom F by NAT_1:45;
then ( F . k in rng F & rng F c= D ) by FUNCT_1:def 5, RELAT_1:def 19;
then reconsider d1 = F . k as Element of D ;
deffunc H₁( Element of NAT ) -> Element of D = f . $1;
consider h being Function of NAT ,D such that
A14: h . k = b . d,d1 and
A15: for n being Element of NAT st n <> k holds
h . n = H₁(n) from FUNCT_2:sch 6();
take a = h . k; :: thesis: ex h being Function of NAT ,D st
( h . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
h . (n + 1) = b . (h . n),(F . (n + 1)) ) & a = h . ((len F) - 1) )
take h = h; :: thesis: ( h . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
h . (n + 1) = b . (h . n),(F . (n + 1)) ) & a = h . ((len F) - 1) )
( h . 0 = f . 0 & 0 in len G & len G = dom G ) by A7, A15, A10, NAT_1:45;
hence h . 0 = F . 0 by A11, FUNCT_1:70; :: thesis: ( ( for n being Element of NAT st n + 1 < len F holds
h . (n + 1) = b . (h . n),(F . (n + 1)) ) & a = h . ((len F) - 1) )
thus for n being Element of NAT st n + 1 < len F holds
h . (n + 1) = b . (h . n),(F . (n + 1)) :: thesis: a = h . ((len F) - 1)

proof

let n be Element of NAT ; :: thesis: ( n + 1 < len F implies h . (n + 1) = b . (h . n),(F . (n + 1)) )
assume A16: n + 1 < len F ; :: thesis: h . (n + 1) = b . (h . n),(F . (n + 1))
A17: n + 1 <= len G by A6, A7, A16, NAT_1:13;

now

per cases ( n + 1 = len G or n + 1 < len G ) by A17, XXREAL_0:1;

suppose n + 1 = len G ; :: thesis: h . (n + 1) = b . (h . n),(F . (n + 1))

then ( n + 1 = k & (n + 1) - 1 = (len G) - 1 & n < k & (n + 1) - 1 = n ) by A7, NAT_1:13;
hence h . (n + 1) = b . (h . n),(F . (n + 1)) by A13, A14, A15; :: thesis: verum

end;

suppose A18: n + 1 < len G ; :: thesis: h . (n + 1) = b . (h . n),(F . (n + 1))

then ( n + 1 in dom G & n <= n + 1 ) by NAT_1:11, NAT_1:45;
then ( G . (n + 1) = F . (n + 1) & f . n = h . n & f . (n + 1) = h . (n + 1) ) by A7, A15, A18, FUNCT_1:70;
hence h . (n + 1) = b . (h . n),(F . (n + 1)) by A12, A18; :: thesis: verum

end;

end;

end;

hence h . (n + 1) = b . (h . n),(F . (n + 1)) ; :: thesis: verum

end;

thus a = h . ((len F) - 1) by A6; :: thesis: verum

end;

end;

end;

hence ex d being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & d = f . ((len F) - 1) ) ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
hence ( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & b₁ = f . ((len F) - 1) ) ) ) by A2; :: thesis: verum

end;

end;

end;

hence ( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT ,D st
( f . 0 = F . 0 & ( for n being Element of NAT st n + 1 < len F holds
f . (n + 1) = b . (f . n),(F . (n + 1)) ) & b₁ = f . ((len F) - 1) ) ) ) ; :: thesis: verum