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: 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 A4: 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 that
A5: len F = k + 1 and
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;
A6: k < k + 1 by NAT_1:13;
then A7: len G = k by A5, 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 A5, 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 A5, 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 A5, 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) )

k < len F by A5, NAT_1:13;
then k in dom F by NAT_1:45;
then A11: F . k in rng F by FUNCT_1:def 5;
rng F c= D by RELAT_1:def 19;
then reconsider d1 = F . k as Element of D by A11;
A12: 0 in len G by A10, NAT_1:45;
consider d being Element of D, f being Function of NAT ,D such that
A13: f . 0 = G . 0 and
A14: for n being Element of NAT st n + 1 < len G holds
f . (n + 1) = b . (f . n),(G . (n + 1)) and
A15: d = f . ((len G) - 1) by A4, A5, A6, A10, AFINSQ_1:14;
deffunc H₁( Element of NAT ) -> Element of D = f . $1;
consider h being Function of NAT ,D such that
A16: h . k = b . d,d1 and
A17: 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 by A7, A10, A17;
hence h . 0 = F . 0 by A13, A12, 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 n + 1 < len F ; :: thesis: h . (n + 1) = b . (h . n),(F . (n + 1))
then A18: n + 1 <= len G by A5, A7, NAT_1:13;

now

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

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

then A20: n < k by A7, NAT_1:13;
n + 1 = k by A5, A6, A19, AFINSQ_1:14;
hence h . (n + 1) = b . (h . n),(F . (n + 1)) by A15, A16, A17, A19, A20; :: thesis: verum

end;

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

then n + 1 in dom G by NAT_1:45;
then A22: G . (n + 1) = F . (n + 1) by FUNCT_1:70;
n <= n + 1 by NAT_1:11;
then A23: f . n = h . n by A7, A17, A21;
f . (n + 1) = h . (n + 1) by A7, A17, A21;
hence h . (n + 1) = b . (h . n),(F . (n + 1)) by A14, A21, A22, A23; :: 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 A5; :: 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;

A24: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A3);
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