let d1, d2 be Element of D; :: thesis: ( ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) & ( ( not b is having_a_unity or not len F = 0 ) & 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)) ) & d1 = f . ((len F) - 1) ) & 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)) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 ) )
thus ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) ; :: thesis: ( ( not b is having_a_unity or not len F = 0 ) & 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)) ) & d1 = f . ((len F) - 1) ) & 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)) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 )
A25: ((len F) - 1) + 1 = len F ;
assume ( not b is having_a_unity or len F <> 0 ) ; :: thesis: ( for f being Function of NAT ,D holds
( not f . 0 = F . 0 or ex n being Element of NAT st
( n + 1 < len F & not f . (n + 1) = b . (f . n),(F . (n + 1)) ) or not d1 = f . ((len F) - 1) ) or for f being Function of NAT ,D holds
( not f . 0 = F . 0 or ex n being Element of NAT st
( n + 1 < len F & not f . (n + 1) = b . (f . n),(F . (n + 1)) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 )
then 0 < len F by A1;
then A26: (len F) - 1 is Element of NAT by NAT_1:20;
given f1 being Function of NAT ,D such that A27: f1 . 0 = F . 0 and
A28: for n being Element of NAT st n + 1 < len F holds
f1 . (n + 1) = b . (f1 . n),(F . (n + 1)) and
A29: d1 = f1 . ((len F) - 1) ; :: thesis: ( for f being Function of NAT ,D holds
( not f . 0 = F . 0 or ex n being Element of NAT st
( n + 1 < len F & not f . (n + 1) = b . (f . n),(F . (n + 1)) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 )
given f2 being Function of NAT ,D such that A30: f2 . 0 = F . 0 and
A31: for n being Element of NAT st n + 1 < len F holds
f2 . (n + 1) = b . (f2 . n),(F . (n + 1)) and
A32: d2 = f2 . ((len F) - 1) ; :: thesis: d1 = d2
defpred S₁[ Element of NAT ] means ( $1 + 1 <= len F implies f1 . $1 = f2 . $1 );
A33: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A34: S₁[n] ; :: thesis: S₁[n + 1]
assume (n + 1) + 1 <= len F ; :: thesis: f1 . (n + 1) = f2 . (n + 1)
then A35: n + 1 < len F by NAT_1:13;
then f2 . (n + 1) = b . (f2 . n),(F . (n + 1)) by A31;
hence f1 . (n + 1) = f2 . (n + 1) by A28, A34, A35; :: thesis: verum

end;

A36: S₁[ 0 ] by A27, A30;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A36, A33);
hence d1 = d2 by A29, A32, A25, A26; :: thesis: verum