now :: 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 sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) ) )

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 sequence of D st
( f . 0 = F . 0 & ( for n being 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 sequence of D st
( f . 0 = F . 0 & ( for n being 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;

suppose A3: 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 sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) ) )

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let F be XFinSequence of D; :: thesis: ( len F = k + 1 & len F <> 0 implies ex d being Element of D ex f being sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) )
assume that
A6: len F = k + 1 and
len F <> 0 ; :: thesis: ex d being Element of D ex f being sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
set G = F | k;
A7: k < k + 1 by NAT_1:13;
then A8: len (F | k) = k by A6, AFINSQ_1:11;

now :: thesis: ex d being Element of D ex f being sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )

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

suppose A9: len (F | k) = 0 ; :: thesis: ex d being Element of D ex f being sequence of D st
( f . 0 = F . 0 & ( for n being 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, A8, CARD_1:49, TARSKI:def 1;
then A10: F . 0 in rng F by FUNCT_1:def 3;
reconsider f = NAT --> (F . 0) as sequence of D by A10, FUNCOP_1:45;
take d = f . 0; :: thesis: ex f being sequence of D st
( f . 0 = F . 0 & ( for n being 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 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:7; :: thesis: ( ( for n being 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 Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) by A6, A8, A9, NAT_1:14; :: thesis: d = f . ((len F) - 1)
k < k + 1 by NAT_1:13;
hence d = f . ((len F) - 1) by A6, A9, AFINSQ_1:11; :: thesis: verum

end;

suppose A11: len (F | k) <> 0 ; :: thesis: ex a being Element of D ex h being sequence of D st
( h . 0 = F . 0 & ( for n being 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 A6, NAT_1:13;
then k in dom F by AFINSQ_1:86;
then A12: F . k in rng F by FUNCT_1:def 3;
reconsider d1 = F . k as Element of D by A12;
A13: 0 in len (F | k) by A11, AFINSQ_1:86;
consider d being Element of D, f being sequence of D such that
A14: f . 0 = (F | k) . 0 and
A15: for n being Nat st n + 1 < len (F | k) holds
f . (n + 1) = b . ((f . n),((F | k) . (n + 1))) and
A16: d = f . ((len (F | k)) - 1) by A5, A6, A7, A11, AFINSQ_1:11;
deffunc H₁( Element of NAT ) -> Element of D = f . $1;
reconsider K = k as Element of NAT by ORDINAL1:def 12;
consider h being sequence of D such that
A17: h . K = b . (d,d1) and
A18: 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 sequence of D st
( h . 0 = F . 0 & ( for n being 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 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 A8, A11, A18;
hence h . 0 = F . 0 by A14, A13, FUNCT_1:47; :: thesis: ( ( for n being 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 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 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 A19: n + 1 <= len (F | k) by A6, A8, NAT_1:13;

now :: thesis: h . (n + 1) = b . ((h . n),(F . (n + 1)))

per cases ( n + 1 = len (F | k) or n + 1 < len (F | k) ) by A19, XXREAL_0:1;

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

then A21: n < k by A8, NAT_1:13;
( n + 1 = k & n in NAT ) by A6, A7, A20, AFINSQ_1:11, ORDINAL1:def 12;
hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A16, A17, A18, A20, A21; :: thesis: verum

end;

suppose A22: n + 1 < len (F | k) ; :: thesis: h . (n + 1) = b . ((h . n),(F . (n + 1)))

then A23: (F | k) . (n + 1) = F . (n + 1) by FUNCT_1:47, AFINSQ_1:86;
( n <= n + 1 & n in NAT ) by NAT_1:11, ORDINAL1:def 12;
then A24: f . n = h . n by A8, A18, A22;
f . (n + 1) = h . (n + 1) by A8, A18, A22;
hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A15, A22, A23, A24; :: 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 sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) ; :: thesis: verum

end;

A25: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A25, 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 sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) ) ) by A1, A3; :: 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 sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) ) ) ; :: thesis: verum