now :: thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
per cases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; :: thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A1; :: thesis: verum
end;
suppose A2: len F <> 0 ; :: thesis: ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) )
defpred S1[ Nat] means for F being FinSequence of D st len F = $1 & len F <> 0 holds
ex d being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) );
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let F be FinSequence 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 . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) )
assume that
A5: len F = k + 1 and
len F <> 0 ; :: thesis: ex d being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
reconsider G = F | (Seg k) as FinSequence of D by FINSEQ_1:18;
A6: len G = k by A5, FINSEQ_3:53;
now :: thesis: ex d being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
per cases ( len G = 0 or len G <> 0 ) ;
suppose A7: len G = 0 ; :: thesis: ex d being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
set f = NAT --> (F . 1);
A8: rng (NAT --> (F . 1)) c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (NAT --> (F . 1)) or x in D )
assume x in rng (NAT --> (F . 1)) ; :: thesis: x in D
then ex y being object st
( y in dom (NAT --> (F . 1)) & (NAT --> (F . 1)) . y = x ) by FUNCT_1:def 3;
then A9: x = F . 1 by FUNCOP_1:7;
1 in dom F by A5, A6, A7, FINSEQ_3:25;
then A10: x in rng F by A9, FUNCT_1:def 3;
rng F c= D by FINSEQ_1:def 4;
hence x in D by A10; :: thesis: verum
end;
dom (NAT --> (F . 1)) = NAT by FUNCOP_1:13;
then reconsider f = NAT --> (F . 1) as sequence of D by A8, RELSET_1:4;
take d = f . 1; :: thesis: ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
take f = f; :: thesis: ( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
thus f . 1 = F . 1 by FUNCOP_1:7; :: thesis: ( ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) )
thus for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) by A5, A6, A7, NAT_1:14; :: thesis: d = f . (len F)
thus d = f . (len F) by A5, A6, A7; :: thesis: verum
end;
suppose A11: len G <> 0 ; :: thesis: ex a being Element of D ex h being sequence of D st
( h . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
reconsider j = len F as Element of NAT ;
1 <= len F by A5, NAT_1:12;
then len F in dom F by FINSEQ_3:25;
then A12: F . (len F) in rng F by FUNCT_1:def 3;
rng F c= D by FINSEQ_1:def 4;
then reconsider t = F . (len F) as Element of D by A12;
len G >= 1 by A11, NAT_1:14;
then A13: 1 in dom G by FINSEQ_3:25;
consider d being Element of D, f being sequence of D such that
A14: f . 1 = G . 1 and
A15: for n being Nat st 0 <> n & n < len G holds
f . (n + 1) = g . ((f . n),(G . (n + 1))) and
A16: d = f . (len G) by A4, A5, A11, FINSEQ_3:53;
deffunc H1( Element of NAT ) -> Element of D = f . $1;
consider h being sequence of D such that
A17: h . j = g . (d,t) and
A18: for n being Element of NAT st n <> j holds
h . n = H1(n) from FUNCT_2:sch 6();
take a = h . j; :: thesis: ex h being sequence of D st
( h . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
take h = h; :: thesis: ( h . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
1 <> j by A5, A11, FINSEQ_3:53;
hence h . 1 = G . 1 by A14, A18
.= F . 1 by A13, FUNCT_1:47 ;
:: thesis: ( ( for n being Nat st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) ) & a = h . (len F) )
thus for n being Nat st 0 <> n & n < len F holds
h . (n + 1) = g . ((h . n),(F . (n + 1))) :: thesis: a = h . (len F)
proof
let n be Nat; :: thesis: ( 0 <> n & n < len F implies h . (n + 1) = g . ((h . n),(F . (n + 1))) )
assume that
A19: n <> 0 and
A20: n < len F ; :: thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
now :: thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
per cases ( n + 1 = len F or n + 1 <> len F ) ;
suppose A21: n + 1 = len F ; :: thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
len G <> len F by A5, A6;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) by A5, A6, A16, A17, A18, A21; :: thesis: verum
end;
suppose A22: n + 1 <> len F ; :: thesis: h . (n + 1) = g . ((h . n),(F . (n + 1)))
n + 1 <= len F by A20, NAT_1:13;
then A23: n + 1 < len F by A22, XXREAL_0:1;
then A24: n < len G by A5, A6, XREAL_1:6;
( 1 <= n + 1 & n + 1 <= len G ) by A5, A6, A23, NAT_1:12, NAT_1:13;
then A25: n + 1 in dom G by FINSEQ_3:25;
h . (n + 1) = f . (n + 1) by A18, A22
.= g . ((f . n),(G . (n + 1))) by A15, A19, A24
.= g . ((f . n),(F . (n + 1))) by A25, FUNCT_1:47
.= g . ((h . (In (n,NAT))),(F . (n + 1))) by A18, A20 ;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; :: thesis: verum
end;
end;
end;
hence h . (n + 1) = g . ((h . n),(F . (n + 1))) ; :: thesis: verum
end;
thus a = h . (len F) ; :: thesis: verum
end;
end;
end;
hence ex d being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d = f . (len F) ) ; :: thesis: verum
end;
A26: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A26, A3);
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) by A2; :: thesis: verum
end;
end;
end;
hence ( ( g is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt g ) & ( ( not g is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & b1 = f . (len F) ) ) ) ; :: thesis: verum